Commit 2024-06-24 21:15 21c5e4e4

feat: lint against stream-of-conciousness obtain syntax (#13220) 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.