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.

## Instances For

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.

## Instances For

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.

## Instances For

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

## Instances For

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.

## Instances For

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)

## Instances For

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