mathlib documentation


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.

inductive tactic.tfae.arrow  :
Instances for tactic.tfae.arrow
meta def tactic.tfae.mk_implication (re : tactic.tfae.arrow) (e₁ e₂ : expr) :
meta def tactic.tfae.mk_name (re : tactic.tfae.arrow) (i₁ i₂ : ) :

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 [...].