Tag lemmas of the form:

@[extensionality]
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 [extensionality [(→),thunk,stream]] funext

Those parameters are cumulative. The following are equivalent:

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

and

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

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

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

Finally, the following:

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

is equivalent to

@[extensionality *]
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 referred to in the lemma statement.

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

ext1 id selects and apply one extensionality lemma (with attribute extensionality), 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.

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.

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