linter.fugue.packUnpack

obtain ⟨a, b, c⟩ : ∃ …, … := ⟨x, y, z⟩ builds an existential out of components that already have names and destructures it on the same line; the ascription then restates types those components already carried. Write the haves.

obtain ⟨…⟩ : T := by tac is a different tactic and stays fine — there the ascription is the tactic block's goal.