mathlib documentation

derive_struct_ext_lemma n generates two extensionality lemmas based on the equality of all non-propositional projections.

On the following:

@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)

derive_struct_lemma generates:

lemma foo.ext : ∀ {α : Type u_1} (x y : foo α),
  x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α),
  x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k

Returns the extensionality lemmas in the environment, as a map from structure name to lemma name.

Returns the extensionality lemmas in the environment, as a list of lemma names.

Tag lemmas of the form:

@[ext]
lemma my_collection.ext (a b : my_collection)
  (h : ∀ x, a.lookup x = b.lookup y) :
  a = b := ...

The attribute indexes extensionality lemma using the type of the objects (i.e. my_collection) which it gets from the statement of the lemma. In some cases, the same lemma can be used to state the extensionality of multiple types that are definitionally equivalent.

attribute [ext [(→),thunk,stream]] funext

Those parameters are cumulative. The following are equivalent:

attribute [ext [(→),thunk]] funext
attribute [ext [stream]] funext

and

attribute [ext [(→),thunk,stream]] funext

One removes type names from the list for one lemma with:

attribute [ext [-stream,-thunk]] funext

Also, the following:

@[ext]
lemma my_collection.ext (a b : my_collection)
  (h : ∀ x, a.lookup x = b.lookup y) :
  a = b := ...

is equivalent to

@[ext *]
lemma my_collection.ext (a b : my_collection)
  (h : ∀ x, a.lookup x = b.lookup y) :
  a = b := ...

This allows us specify type synonyms along with the type that is referred to in the lemma statement.

@[ext [*,my_type_synonym]]
lemma my_collection.ext (a b : my_collection)
  (h : ∀ x, a.lookup x = b.lookup y) :
  a = b := ...

The ext attribute can be applied to a structure to generate its extensionality lemmas:

@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)

will generate:

@[ext] lemma foo.ext : ∀ {α : Type u_1} (x y : foo α),
x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α),
x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k

ext1 id selects and apply one extensionality lemma (with attribute ext), using id, if provided, to name a local constant introduced by the lemma. If id is omitted, the local constant is named automatically, as per intro.

• ext applies as many extensionality lemmas as possible;
• ext ids, with ids a list of identifiers, finds extentionality and applies them until it runs out of identifiers in ids to name the local constants.
• ext can also be given an rcases pattern in place of an identifier. This will destruct the introduced local constant.

When trying to prove:

α β : Type,
f g : α → set β
⊢ f = g

applying ext x y yields:

α β : Type,
f g : α → set β,
x : α,
y : β
⊢ y ∈ f x ↔ y ∈ f x

by applying functional extensionality and set extensionality.

When trying to prove:

α β γ : Type
f g : α × β → γ
⊢ f = g

applying ext ⟨a, b⟩ yields:

α β γ : Type,
f g : α × β → γ,
a : α,
b : β
⊢ f (a, b) = g (a, b)

by applying functional extensionality and destructing the introduced pair.

A maximum depth can be provided with ext x y z : 3.