- right : tactic.tfae.arrow
- left_right : tactic.tfae.arrow
- left : tactic.tfae.arrow
def
tactic.interactive.tfae_have
:
interactive.parse (optional lean.parser.ident <* lean.parser.tk ":") → interactive.parse (interactive.with_desc ↑"i" lean.parser.small_nat) → interactive.parse ((lean.parser.tk "→" <|> lean.parser.tk "->") *> return tactic.tfae.arrow.right <|> (lean.parser.tk "↔" <|> lean.parser.tk "<->") *> return tactic.tfae.arrow.left_right <|> (lean.parser.tk "←" <|> lean.parser.tk "<-") *> return tactic.tfae.arrow.left) → interactive.parse (interactive.with_desc ↑"j" lean.parser.small_nat) → (tactic unit := tactic.solve_by_elim) → tactic unit
In a goal of the form tfae [a₀, a₁, a₂],
tfae_have : i → j creates the assertion aᵢ → aⱼ. The other possible
notations are tfae_have : i ← j and tfae_have : i ↔ j. The user can
also provide a label for the assertion, as with have: tfae_have h : i ↔ j.
Finds all implications and equivalences in the context
to prove a goal of the form tfae [...].