def Lean.Parser.Attr.extIff : Lean.ParserDescr

The flag (iff := false) prevents ext from generating an ext_iff lemma.

Equations

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

def Lean.Parser.Attr.extFlat : Lean.ParserDescr

The flag (flat := false) causes ext to not flatten parents' fields when generating an ext lemma.

Equations

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

def Lean.Parser.Attr.ext : Lean.ParserDescr

Registers an extensionality theorem.

• When @[ext] is applied to a theorem, the theorem is registered for the ext tactic, and it generates an "ext_iff" theorem. The name of the theorem is from adding the suffix _iff to the theorem name.

• When @[ext] is applied to a structure, it generates an .ext theorem and applies the @[ext] attribute to it. The result is an .ext and an .ext_iff theorem with the .ext theorem registered for the ext tactic.

• An optional natural number argument, e.g. @[ext 9000], specifies a priority for the ext lemma. Higher-priority lemmas are chosen first, and the default is 1000.

• The flag @[ext (iff := false)] disables generating an ext_iff theorem.

• The flag @[ext (flat := false)] causes generated structure extensionality theorems to show inherited fields based on their representation, rather than flattening the parents' fields into the lemma's equality hypotheses.

Equations

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

def Lean.Elab.Tactic.Ext.ext : Lean.ParserDescr

Applies extensionality lemmas that are registered with the @[ext] attribute.

• ext pat* applies extensionality theorems as much as possible, using the patterns pat* to introduce the variables in extensionality theorems using rintro. For example, the patterns are used to name the variables introduced by lemmas such as funext.
• Without patterns,ext applies extensionality lemmas as much as possible but introduces anonymous hypotheses whenever needed.
• ext pat* : n applies ext theorems only up to depth n.

The ext1 pat* tactic is like ext pat* except that it only applies a single extensionality theorem.

Unused patterns will generate warning. Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.

Equations

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

def Lean.Elab.Tactic.Ext.applyExtTheorem : Lean.ParserDescr

Apply a single extensionality theorem to the current goal.

Equations

• Lean.Elab.Tactic.Ext.applyExtTheorem = Lean.ParserDescr.node `Lean.Elab.Tactic.Ext.applyExtTheorem 1024 (Lean.ParserDescr.nonReservedSymbol "apply_ext_theorem" false)

def Lean.Elab.Tactic.Ext.tacticExt1___ : Lean.ParserDescr

ext1 pat* is like ext pat* except that it only applies a single extensionality theorem rather than recursively applying as many extensionality theorems as possible.

The pat* patterns are processed using the rintro tactic. If no patterns are supplied, then variables are introduced anonymously using the intros tactic.

Equations

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

theorem PSigma.ext {α : Sort u} {β : α → Sort v} {x : PSigma β} {y : PSigma β} (fst : x.fst = y.fst) (snd : HEq x.snd y.snd) : x = y

theorem PSigma.ext_iff {α : Sort u} {β : α → Sort v} {x : PSigma β} {y : PSigma β} : x = y ↔ x.fst = y.fst ∧ HEq x.snd y.snd

theorem PProd.ext {α : Sort u} {β : Sort v} {x : α ×' β} {y : α ×' β} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

theorem Sigma.ext_iff {α : Type u} {β : α → Type v} {x : Sigma β} {y : Sigma β} : x = y ↔ x.fst = y.fst ∧ HEq x.snd y.snd

theorem Prod.ext {α : Type u} {β : Type v} {x : α × β} {y : α × β} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

theorem PProd.ext_iff {α : Sort u} {β : Sort v} {x : α ×' β} {y : α ×' β} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

theorem Sigma.ext {α : Type u} {β : α → Type v} {x : Sigma β} {y : Sigma β} (fst : x.fst = y.fst) (snd : HEq x.snd y.snd) : x = y

theorem Prod.ext_iff {α : Type u} {β : Type v} {x : α × β} {y : α × β} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

theorem propext_iff {a : Prop} {b : Prop} : a = b ↔ (a ↔ b)

theorem Subtype.eq_iff {α : Type u} {p : α → Prop} {a1 : { x : α // p x }} {a2 : { x : α // p x }} : a1 = a2 ↔ a1.val = a2.val

theorem funext_iff {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} : f = g ↔ ∀ (x : α), f x = g x

theorem PUnit.ext_iff {x : PUnit} {y : PUnit} : x = y ↔ True

theorem PUnit.ext (x : PUnit) (y : PUnit) : x = y

theorem Unit.ext (x : Unit) (y : Unit) : x = y