Similar to #11045; discovered in #12834.

Similar to #11045; discovered in #12834.

Similar to #11045; discovered in #12834.

Concludes the work started in (TTBOMK) #11045 and #12850.
To make sure this is exhaustive, I wrote a syntax linter for this, which I will propose separately.

This uncovered some interesting interactions with the multi-goal linter:
in a few instances, about using the newer syntax, the sub-goal focusing also became obsolete.

Concludes the work started in (TTBOMK) #11045 and #12850.
To make sure this is exhaustive, I wrote a syntax linter for this, which I will propose separately.

This uncovered some interesting interactions with the multi-goal linter:
in a few instances, about using the newer syntax, the sub-goal focusing also became obsolete.

Concludes the work started in (TTBOMK) #11045 and #12850.
To make sure this is exhaustive, I wrote a syntax linter for this, which I will propose separately.

This uncovered some interesting interactions with the multi-goal linter:
in a few instances, about using the newer syntax, the sub-goal focusing also became obsolete.

Just the syntax replacements are split into #13219.

Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances.

**Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534:
- it's a Lean3-ism, which can be unlearned now
- the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact`
- when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot
(This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) 
- the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer.

Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all,
but moves forward with something that is doable within mathlib today.

Just the syntax replacements are split into #13219.

Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances.

**Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534:
- it's a Lean3-ism, which can be unlearned now
- the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact`
- when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot
(This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) 
- the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer.

Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all,
but moves forward with something that is doable within mathlib today.

Just the syntax replacements are split into #13219.

Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances.

**Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534:
- it's a Lean3-ism, which can be unlearned now
- the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact`
- when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot
(This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) 
- the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer.

Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all,
but moves forward with something that is doable within mathlib today.