The Following Are Equivalent (TFAE) #
This file provides the tactics
tfae_finish for proving the pairwise equivalence of
propositions in a set using various implications between them.
In a goal of the form
tfae [a₀, a₁, a₂],
tfae_have : i → j creates the assertion
aᵢ → aⱼ. The other possible
tfae_have : i ← j and
tfae_have : i ↔ j. The user can
also provide a label for the assertion, as with
tfae_have h : i ↔ j.