def Std.Tactic.Ext.withExtHyps {α : Type} (struct : Lean.Name) (flat : Lean.Term) (k : Array Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.Name × Lean.Expr) → Lean.MetaM α) : Lean.MetaM α

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.

def Std.Tactic.Ext.«termExt_type%___» : Lean.ParserDescr

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.

def Std.Tactic.Ext.mkIff (p : Lean.Expr) (q : Lean.Expr) : Lean.Expr

Make an Iff application.

Equations

• Std.Tactic.Ext.mkIff p q = Lean.mkApp2 (Lean.mkConst `Iff) p q

def Std.Tactic.Ext.mkAndN : List Lean.Expr → Lean.Expr

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

Equations

• Std.Tactic.Ext.mkAndN [] = Lean.mkConst `True
• Std.Tactic.Ext.mkAndN [p] = p
• Std.Tactic.Ext.mkAndN (p :: ps) = Lean.mkAnd p (Std.Tactic.Ext.mkAndN ps)

def Std.Tactic.Ext.«termExt_iff_type%___» : Lean.ParserDescr

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.

def Std.Tactic.Ext.applyExtLemma (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Apply a single extensionality lemma to goal.

Equations

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

def Std.Tactic.Ext.tacticApply_ext_lemma : Lean.ParserDescr

Apply a single extensionality lemma to the current goal.

Equations

• Std.Tactic.Ext.tacticApply_ext_lemma = Lean.ParserDescr.node `Std.Tactic.Ext.tacticApply_ext_lemma 1024 (Lean.ParserDescr.nonReservedSymbol "apply_ext_lemma" false)

def Std.Tactic.Ext.tryIntros {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) : m Nat

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.
• Std.Tactic.Ext.tryIntros g [] k = do let __do_lift ← liftM (liftM (Lean.MVarId.intros g)) k __do_lift.snd []

def Std.Tactic.Ext.withExt1 {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) : m Nat

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 : Type → Type u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] [MonadExcept Lean.Exception m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m Nat) (depth : optParam Nat 1000000) (failIfUnchanged : optParam Bool true) : m Nat

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 : optParam Bool true) : Lean.Elab.TermElabM (Nat × Array (Lean.MVarId × List (Lean.TSyntax `rcasesPat)))

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

Equations

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

def Std.Tactic.Ext.«tacticExt___:_» : Lean.ParserDescr

• ext pat* applies extensionality lemmas as much as possible, using pat* to introduce the variables in extensionality lemmas using rintro. For example, this names the variables introduced by lemmas such as funext.
• ext applies extensionality lemmas as much as possible but introduces anonymous variables whenever needed.
• ext pat* : n applies ext lemmas only up to depth n.

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

The ext? tactic (note: unimplemented) has the same syntax as the ext tactic, and it gives a suggestion of an equivalent tactic to use in place of ext.

Equations

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

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

ext1 pat* is like ext pat* except that it only applies a single extensionality lemma rather than recursively applying as many extensionality lemmas 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.

The ext1? tactic (note: unimplemented) has the same syntax as the ext1? tactic, and it gives a suggestion of an equivalent tactic to use in place of ext1.

Equations

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

def Std.Tactic.Ext.tacticExt1?___ : Lean.ParserDescr

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.

def Std.Tactic.Ext.«tacticExt?___:_» : Lean.ParserDescr

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 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