Lean4
/-- `tfae_finish` is used to close goals of the form `TFAE [P₁, P₂, ...]` once a sufficient collection
of hypotheses of the form `Pᵢ → Pⱼ` or `Pᵢ ↔ Pⱼ` have been introduced to the local context.
`tfae_have` can be used to conveniently introduce these hypotheses; see `tfae_have`.
Example:
```lean4
example : TFAE [P, Q, R] := by
tfae_have 1 → 2 := sorry /- proof of P → Q -/
tfae_have 2 → 1 := sorry /- proof of Q → P -/
tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
tfae_finish
```
-/
@[tactic_parser 1000]
public meta def tfaeFinish : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.TFAE.tfaeFinish 1024 (ParserDescr.nonReservedSymbol✝ "tfae_finish" false✝)
