.. _tac_ext:

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

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

.. code-block::

   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

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

.. code-block::

   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.