mathlib documentation

tactic.tfae

The Following Are Equivalent (TFAE) #

This file provides the tactics tfae_have and tfae_finish for proving the pairwise equivalence of propositions in a set using various implications between them.

source
@[protected, instance]
def tactic.tfae.arrow.inhabited  :
inhabited tactic.tfae.arrow
source
@[protected, instance]
meta def tactic.tfae.arrow.has_reflect  :
has_reflect tactic.tfae.arrow
source
inductive tactic.tfae.arrow  :
Type
source
meta def tactic.tfae.mk_implication (re : tactic.tfae.arrow) (e₁ e₂ : expr) :
pexpr
source
meta def tactic.tfae.mk_name (re : tactic.tfae.arrow) (i₁ i₂ : ℕ) :
name
source
meta def tactic.interactive.parse_list  :
expr → option (list expr)
source
meta def tactic.interactive.tfae_have (h : interactive.parse (lean.parser.ident? <* lean.parser.tk ":")) (i₁ : interactive.parse (interactive.with_desc ↑"i" lean.parser.small_nat)) (re : 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)) (i₂ : interactive.parse (interactive.with_desc ↑"j" lean.parser.small_nat)) :
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.

source
meta def tactic.interactive.tfae_finish  :
tactic unit

Finds all implications and equivalences in the context to prove a goal of the form tfae [...].