The Following Are Equivalent (TFAE)

This file provides the tactics tfae_have and tfae_finish for proving goals of the form TFAE [P₁, P₂, ...].

def Mathlib.Tactic.TFAE.impArrow : Lean.ParserDescr

An arrow of the form ←, →, or ↔.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.TFAE.tfaeHave : Lean.ParserDescr

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 TFAE goal list. A proof is required afterward, typically via a tactic block.

example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3
  · exact h
  ...

The resulting context now includes tfae_1_to_3 : P → R.

The introduced hypothesis can be given a custom name, in analogy to have syntax:

tfae_have h : 2 ↔ 3

Once sufficient hypotheses have been introduced by tfae_have, tfae_finish can be used to close the goal.

example : TFAE [P, Q, R] := by
  tfae_have 1 → 2
  · /- proof of P → Q -/
  tfae_have 2 → 1
  · /- proof of Q → P -/
  tfae_have 2 ↔ 3
  · /- proof of Q ↔ R -/
  tfae_finish

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.TFAE.tfaeFinish : Lean.ParserDescr

tfae_finish is used to close goals of the form TFAE [P₁, P₂, ...] once a sufficient collection of hypotheses of the form Pᵢ → Pⱼ or Pᵢ ↔ Pⱼ have been introduced to the local context.

tfae_have can be used to conveniently introduce these hypotheses; see tfae_have.

Example:

example : TFAE [P, Q, R] := by
  tfae_have 1 → 2
  · /- proof of P → Q -/
  tfae_have 2 → 1
  · /- proof of Q → P -/
  tfae_have 2 ↔ 3
  · /- proof of Q ↔ R -/
  tfae_finish

Equations

• Mathlib.Tactic.TFAE.tfaeFinish = Lean.ParserDescr.node `Mathlib.Tactic.TFAE.tfaeFinish 1024 (Lean.ParserDescr.nonReservedSymbol "tfae_finish" false)

Setup

def Mathlib.Tactic.TFAE.getTFAEList (t : Lean.Expr) : Lean.MetaM (Q(List Prop) × List Q(Prop))

Extract a list of Prop expressions from an expression of the form TFAE [P₁, P₂, ...] as long as [P₁, P₂, ...] is an explicit list.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.TFAE.getTFAEList.getExplicitList (l : Q(List Prop)) : Lean.MetaM (List Q(Prop))

Convert an expression representing an explicit list into a list of expressions.

Proof construction

partial def Mathlib.Tactic.TFAE.dfs (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (i : ℕ) (j : ℕ) (P : Q(Prop)) (P' : Q(Prop)) (hP : Q(«$P»)) : StateT (Std.HashSet ℕ) Lean.MetaM Q(«$P'»)

Uses depth-first search to find a path from P to P'.

def Mathlib.Tactic.TFAE.proveImpl (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (i : ℕ) (j : ℕ) (P : Q(Prop)) (P' : Q(Prop)) : Lean.MetaM Q(«$P» → «$P'»)

Prove an implication via depth-first traversal.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.TFAE.proveChain (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (i : ℕ) (is : List ℕ) (P : Q(Prop)) (l : Q(List Prop)) : Lean.MetaM Q(List.Chain (fun (x1 x2 : Prop) => x1 → x2) «$P» «$l»)

Generate a proof of Chain (· → ·) P l. We assume P : Prop and l : List Prop, and that l is an explicit list.

partial def Mathlib.Tactic.TFAE.proveGetLastDImpl (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (i : ℕ) (i' : ℕ) (is : List ℕ) (P : Q(Prop)) (P' : Q(Prop)) (l : Q(List Prop)) : Lean.MetaM Q(«$l».getLastD «$P'» → «$P»)

Attempt to prove getLastD l P' → P given an explicit list l.

def Mathlib.Tactic.TFAE.proveTFAE (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (is : List ℕ) (l : Q(List Prop)) : Lean.MetaM Q(«$l».TFAE)

Attempt to prove a statement of the form TFAE [P₁, P₂, ...].

tfae_have components

def Mathlib.Tactic.TFAE.mkTFAEHypName (i : Lean.TSyntax `num) (j : Lean.TSyntax `num) (arr : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) : Lean.MetaM Lean.Name

Construct a name for a hypothesis introduced by tfae_have.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.TFAE.tfaeHaveCore (goal : Lean.MVarId) (name : Option (Lean.TSyntax `ident)) (i : Lean.TSyntax `num) (j : Lean.TSyntax `num) (arrow : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) (t : Lean.Expr) : Lean.Elab.TermElabM (Lean.MVarId × Lean.MVarId)

The core of tfae_have, which behaves like haveLetCore in Mathlib.Tactic.Have.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.TFAE.elabIndex (i : Lean.TSyntax `num) (maxIndex : ℕ) : Lean.Elab.Tactic.TacticM ℕ

Turn syntax for a given index into a natural number, as long as it lies between 1 and maxIndex.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.TFAE.mkImplType (Pi : Q(Prop)) (arr : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) (Pj : Q(Prop)) : Lean.MetaM Q(Prop)

Construct an expression for the type Pj → Pi, Pi → Pj, or Pi ↔ Pj given expressions Pi Pj : Q(Prop) and impArrow syntax arr, depending on whether arr is ←, →, or ↔ respectively.

Equations

• One or more equations did not get rendered due to their size.

Tactic implementation