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

Registers an extensionality theorem.

• When @[ext] is applied to a structure, it generates .ext and .ext_iff theorems and registers them for the ext tactic.

• When @[ext] is applied to a theorem, the theorem is registered for the ext tactic.

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

• 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. structures in the generated extensionality theorems.

Equations

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

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

Creates the type of the extensionality theorem for the given structure, elaborating to x.1 = y.1 → x.2 = y.2 → x = y, for example.

Equations

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

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

Creates the type of the iff-variant of the extensionality theorem for the given structure, elaborating to x = y ↔ x.1 = y.1 ∧ x.2 = y.2, for example.

Equations

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

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

declare_ext_theorems_for A declares the extensionality theorems for the structure A.

These theorems state that two expressions with the structure type are equal if their fields are equal.

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 Prod.ext {α : Type u_1} {β : Type u_2} {x : α × β} {y : α × β} : x.fst = y.fst → x.snd = y.snd → x = y

theorem PProd.ext {α : Sort u_1} {β : Sort u_2} {x : PProd α β} {y : PProd α β} : x.fst = y.fst → x.snd = y.snd → x = y

theorem Sigma.ext : ∀ {α : Type u_1} {β : α → Type u_2} {x y : Sigma β}, x.fst = y.fst → HEq x.snd y.snd → x = y

theorem PSigma.ext : ∀ {α : Sort u_1} {β : α → Sort u_2} {x y : PSigma β}, x.fst = y.fst → HEq x.snd y.snd → x = y

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

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