Lean4
Module 6 · Lesson 4

ext & funext

Apply extensionality principles to prove equality.ext proves two things equal by showing their components or behaviors are equal.

❗
ext in its full power requires Mathlib. The basic funext is available in core Lean 4.

Function Extensionality

lean
1-- Two functions are equal if they give equal outputs for all inputs
2-- This is funext, available in core Lean
3
4example : (fun x : Nat => x + 0) = (fun x => x) := by
5  funext x
6  -- Goal: x + 0 = x
7  simp
8
9example : (fun x : Nat => x * 1) = (fun x => x) := by
10  funext x
11  ring
Key Takeaway
funext x transforms a goalf = g into proving f x = g xfor an arbitrary x.

The ext Tactic

lean
1import Mathlib.Tactic.Ext
2
3-- ext is more powerful - works for any type with @[ext] lemmas
4example : (fun x : Nat => x + 0) = (fun x => x) := by
5  ext x
6  simp
7
8-- ext works on structures too
9example (p q : Nat × Nat) (h1 : p.1 = q.1) (h2 : p.2 = q.2) : p = q := by
10  ext
11  · exact h1  -- First component
12  · exact h2  -- Second component

Set Extensionality

lean
1import Mathlib.Tactic.Ext
2import Mathlib.Data.Set.Basic
3
4-- Two sets are equal if they have the same elements
5example (A B : Set Nat) (h : ∀ x, x ∈ A ↔ x ∈ B) : A = B := by
6  ext x
7  exact h x
8
9-- Proving set equalities
10example : ({1, 2} : Set Nat) = {2, 1} := by
11  ext x
12  simp [Set.mem_insert_iff]
13  tauto

Structure Extensionality

lean
1import Mathlib.Tactic.Ext
2
3-- Structures are equal if all fields are equal
4structure Point where
5  x : Float
6  y : Float
7
8-- @[ext] generates an extensionality lemma
9@[ext]
10theorem Point.ext_iff (p q : Point) : p = q ↔ p.x = q.x ∧ p.y = q.y := by
11  constructor
12  · intro h; simp [h]
13  · intro ⟨hx, hy⟩; cases p; cases q; simp_all
14
15example (p q : Point) (hx : p.x = q.x) (hy : p.y = q.y) : p = q := by
16  ext
17  · exact hx
18  · exact hy
ℹ
Mark your structures with @[ext] to automatically generate extensionality lemmas that extcan use.

Multiple Variables

lean
1import Mathlib.Tactic.Ext
2
3-- ext can introduce multiple variables
4example : (fun x y : Nat => x + y) = (fun x y => y + x) := by
5  ext x y
6  ring
7
8-- Or one at a time
9example : (fun x y : Nat => x + y) = (fun x y => y + x) := by
10  ext x
11  ext y
12  ring
Deep Dive: How ext Works

ext looks for lemmas tagged with@[ext] that match the goal type:

lean
1-- For functions: funext
2-- For sets: Set.ext
3-- For products: Prod.ext
4-- For structures: generated by @[ext]
5
6-- The lemma should have the form:
7-- (∀ components are equal) → whole is equal

ext with Patterns

lean
1import Mathlib.Tactic.Ext
2
3-- You can name and pattern-match the introduced variable
4example : (fun p : Nat × Nat => p.1 + p.2) = (fun p => p.2 + p.1) := by
5  ext ⟨a, b⟩
6  ring
7
8-- Or use wildcards
9example : (fun _ : Nat => 0) = (fun _ => 0) := by
10  ext _
11  rfl

Real-World Examples

Proving Function Compositions Equal

lean
1import Mathlib.Tactic.Ext
2
3-- (f ∘ id) = f
4example (f : Nat → Nat) : (fun x => f (id x)) = f := by
5  ext x
6  rfl
7
8-- (id ∘ f) = f
9example (f : Nat → Nat) : (fun x => id (f x)) = f := by
10  ext x
11  rfl

Set Algebra

lean
1import Mathlib.Tactic.Ext
2import Mathlib.Data.Set.Basic
3
4-- A ∩ B = B ∩ A
5example (A B : Set α) : A ∩ B = B ∩ A := by
6  ext x
7  constructor
8  · intro ⟨ha, hb⟩; exact ⟨hb, ha⟩
9  · intro ⟨hb, ha⟩; exact ⟨ha, hb⟩

Vector Space Operations

lean
1import Mathlib.Tactic.Ext
2
3-- Prove two linear maps are equal
4-- (Would need more imports for real linear maps)
5example (f g : Nat → Nat) (h : ∀ n, f n = g n) : f = g := by
6  ext n
7  exact h n

ext vs funext

lean
1-- funext: core Lean, functions only
2example : (fun x : Nat => x) = (fun x => x) := by
3  funext x
4  rfl
5
6-- ext: Mathlib, works on more types
7-- - Functions (uses funext)
8-- - Sets (uses Set.ext)
9-- - Structures (uses generated lemmas)
10-- - Products, subtypes, etc.
11
12-- Prefer ext when available for its generality
contraposeNext: congr