def Lean.Parser.Attr.extIff : ParserDescr

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

def Lean.Parser.Attr.extFlat : ParserDescr

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

def Lean.Parser.Attr.ext : 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.

def Lean.Elab.Tactic.Ext.ext : 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.

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

Apply a single extensionality theorem to the current goal.

def Lean.Elab.Tactic.Ext.tacticExt1___ : 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.

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

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

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

theorem Prod.ext_iff {α : Type u} {β : Type v} {x y : α × β} : x = y ↔ x.fst = y.fst ∧ 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 PSigma.ext {α : Sort u} {β : α → Sort v} {x y : PSigma β} (fst : x.fst = y.fst) (snd : x.snd ≍ y.snd) : x = y

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

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

theorem Char.ext_iff {c d : Char} : c = d ↔ c.val = d.val

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

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

theorem Array.ext_iff {α : Type u} {xs ys : Array α} : xs = ys ↔ xs.size = ys.size ∧ ∀ (i : Nat) (hi₁ : i < xs.size) (hi₂ : i < ys.size), xs[i] = ys[i]

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

@[deprecated Subtype.ext_iff (since := "2025-10-26")]

def Subtype.eq_iff {α : Sort u_1} {p : α → Prop} {a1 a2 : { x : α // p x }} : a1 = a2 ↔ a1.val = a2.val

theorem PUnit.ext_iff {a b : PUnit} : a = b ↔ True

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

theorem Thunk.ext {α : Type u_1} {a b : Thunk α} : a.get = b.get → a = b

theorem Thunk.ext_iff {α : Type u_1} {a b : Thunk α} : a = b ↔ a.get = b.get