# Documentation

Std.Tactic.Ext

def Std.Tactic.Ext.withExtHyps {α : Type} (struct : Lean.Name) (k : ) :

Constructs the hypotheses for the extensionality lemma. Calls the continuation k with the list of parameters to the structure, two structure variables x and y, and a list of pairs (field, ty) where ty is x.field = y.field or HEq x.field y.field.

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

Creates the type of the extensionality lemma 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.

Make an Iff application.

Equations

Make an n-ary And application. mkAndN [] returns True.

Equations

Creates the type of the iff-variant of the extensionality lemma 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.

Apply a single extensionality lemma to goal.

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

Apply a single extensionality lemma to the current goal.

Equations
def Std.Tactic.Ext.tryIntros {m : TypeType u_1} [inst : ] [inst : ] (g : Lean.MVarId) (pats : List (Lean.TSyntax rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax rcasesPat)m Unit) :

Postprocessor for withExt which runs rintro with the given patterns when the target is a pi type.

Equations
• One or more equations did not get rendered due to their size.
def Std.Tactic.Ext.withExt1 {m : TypeType u_1} [inst : ] [inst : ] (g : Lean.MVarId) (pats : List (Lean.TSyntax rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax rcasesPat)m Unit) :

Applies a single extensionality lemma, using pats to introduce variables in the result. Runs continuation k on each subgoal.

Equations
• One or more equations did not get rendered due to their size.
def Std.Tactic.Ext.withExtN {m : TypeType u_1} [inst : ] [inst : ] [inst : ] (g : Lean.MVarId) (pats : List (Lean.TSyntax rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax rcasesPat)m Unit) (depth : optParam Nat 1000000) (failIfUnchanged : ) :

Applies a extensionality lemmas recursively, using pats to introduce variables in the result. Runs continuation k on each subgoal.

Equations
• One or more equations did not get rendered due to their size.
• Std.Tactic.Ext.withExtN g pats k 0 failIfUnchanged = k g pats
def Std.Tactic.Ext.extCore (g : Lean.MVarId) (pats : List (Lean.TSyntax rcasesPat)) (depth : optParam Nat 1000000) (failIfUnchanged : ) :

Apply extensionality lemmas as much as possible, using pats to introduce the variables in extensionality lemmas like funext. Returns a list of subgoals, and the unconsumed patterns in each of those subgoals.

Equations
• One or more equations did not get rendered due to their size.
• ext pat*: Apply extensionality lemmas as much as possible, using pat* to introduce the variables in extensionality lemmas like funext.
• ext: introduce anonymous variables whenever needed.
Equations
• One or more equations did not get rendered due to their size.

ext1 pat* is like ext pat* except it only applies one extensionality lemma instead of recursing as much as possible.

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

ext1? pat* is like ext1 pat* but gives a suggestion on what pattern to use

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

ext? pat* is like ext pat*` but gives a suggestion on what pattern to use

Equations
• One or more equations did not get rendered due to their size.
theorem PUnit.ext (x : PUnit) (y : PUnit) :
x = y
theorem Unit.ext (x : Unit) (y : Unit) :
x = y