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 subsets of a type are the same if they have the same elements, two subgroups of a group 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 Mathlib.Tactic

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

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

import Mathlib.Tactic

example (G : Type) [Group G] (K L : Subgroup G)
    (h : ∀ a, a ∈ K ↔ a ∈ L) : K = L := by
  -- ⊢ K = L
  ext g
  -- ⊢ g ∈ K ↔ g ∈ L
  apply h
  done

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 it’s exactly the theorem that if ∀ (x : G), x ∈ H ↔ x ∈ K then H = K. This theorem was tagged with @[ext] when it was defined, 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.