ext

Summary

The ext tactic applies “extensionality lemmas”. An extensionality lemma says “two things are the same if they are built from the same stuff”. Examples: two sets are the same if they have the same elements, two subgroups are the same if they have the same elements, two functions are the same if they take the same values on all inputs, two group homomorphisms are the same if they take the same values on all inputs.

Examples

Here we use the ext tactic to prove that two group homomorphisms are equal if they take the same values on all inputs.

import group_theory.subgroup.basic

example (G H : Type) [group G] [group H] (φ ψ : G →* H)
  (h : ∀ a, φ a = ψ a) : φ = ψ :=
begin
  -- ⊢ φ = ψ
  ext g,
  -- ⊢ ⇑φ g = ⇑ψ g
  apply h, -- goals accomplished
end

Here we use it to prove that two subgroups of a group are equal if they contain the same elements.

import group_theory.subgroup.basic

example (G : Type) [group G] (K L : subgroup G)
  (h : ∀ a, a ∈ K ↔ a ∈ L) : K = L :=
begin
  -- ⊢ K = L
  ext g,
  -- ⊢ g ∈ K ↔ g ∈ L
  apply h, -- goals accomplished
end

Details

What the ext tactic does is it tries to apply lemmas which are tagged with the @[ext] attribute. For example if you try #check @subgroup.ext you can see that in the second example above, ext g does the same thing as apply subgroup.ext, intro g. Furthermore, if you try #print subgroup.ext, you’ll see a list at the very top of the output, starting with an @, and somewhere in that list is the word ext, meaning that subgroup.ext is tagged with the @[ext] attribute, which is why the ext tactic makes progress on the goal.

Further notes

Sometimes ext applies more lemmas than you want it to do. In this case you can use the less aggressive tactic ext1, which only applies one lemma.