Lean4
/-- `tfae_have` introduces hypotheses for proving goals of the form `TFAE [P₁, P₂, ...]`. Specifically,
`tfae_have i <arrow> j := ...` introduces a hypothesis of type `Pᵢ <arrow> Pⱼ` to the local
context, where `<arrow>` can be `→`, `←`, or `↔`. Note that `i` and `j` are natural number indices
(beginning at 1) used to specify the propositions `P₁, P₂, ...` that appear in the goal.
```lean4
example (h : P → R) : TFAE [P, Q, R] := by
tfae_have 1 → 3 := h
...
```
The resulting context now includes `tfae_1_to_3 : P → R`.
Once sufficient hypotheses have been introduced by `tfae_have`, `tfae_finish` can be used to close
the goal. For 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
```
All features of `have` are supported by `tfae_have`, including naming, matching,
destructuring, and goal creation. These are demonstrated below.
```lean4
example : TFAE [P, Q] := by
-- assert `tfae_1_to_2 : P → Q`:
tfae_have 1 → 2 := sorry
-- assert `hpq : P → Q`:
tfae_have hpq : 1 → 2 := sorry
-- match on `p : P` and prove `Q` via `f p`:
tfae_have 1 → 2
| p => f p
-- assert `pq : P → Q`, `qp : Q → P`:
tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry
-- assert `h : P → Q`; `?a` is a new goal:
tfae_have h : 1 → 2 := f ?a
...
```
-/
@[tactic_parser 1000]
public meta def tfaeHave : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.TFAE.tfaeHave 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "tfae_have " false✝)
(ParserDescr.parser✝
(Lean.Name.mkStr✝
(Lean.Name.mkStr✝
(Lean.Name.mkStr✝
(Lean.Name.mkStr✝
(Lean.Name.mkStr✝
(Lean.Name.mkNum✝
(Lean.Name.mkStr✝
(Lean.Name.mkStr✝ (Lean.Name.mkStr✝ (Lean.Name.mkStr✝ Lean.Name.anonymous✝ "_private") "Mathlib")
"Tactic")
"TFAE")
0)
"Mathlib")
"Tactic")
"TFAE")
"Parser")
"tfaeHaveDecl")))
