lean-tp-quantifiers

name: lean-tp-quantifiers description: Universal/existential quantifiers and equality reasoning. Use when proving forall/exists, equational reasoning with rfl, calc chains, or substitution. allowed-tools: Read, Grep, Glob

Lean 4 Quantifiers and Equality

Universal/existential quantifiers and equality reasoning. Use when proving properties for all values, existence claims, or equational reasoning.

Trigger terms: "forall", "exists", "∀", "∃", "equality", "rfl", "calc", "rewrite", "subst"

Universal Quantifier (∀)

Syntax: ∀ x : α, p x (same as (x : α) → p x)

Introduction - Prove for arbitrary value:

example : ∀ x : Nat, x + 0 = x := fun x => rfl

-- In tactic mode
example : ∀ x : Nat, x + 0 = x := by
  intro x
  rfl

Elimination - Apply to specific term:

-- Given h : ∀ x, p x and t : Nat
-- Get: h t : p t

Existential Quantifier (∃)

Syntax: ∃ x : α, p x

Introduction - Provide witness:

example : ∃ x : Nat, x > 0 := ⟨1, Nat.one_pos⟩

-- Or use 'use' tactic
example : ∃ x : Nat, x > 0 := by
  use 1
  decide

Elimination - Extract witness:

example (h : ∃ x, p x) : q := by
  match h with
  | ⟨w, hw⟩ => -- w is witness, hw : p w
    ...

-- Or with obtain
example (h : ∃ x, p x) : q := by
  obtain ⟨w, hw⟩ := h
  ...

Equality

Reflexivity - rfl proves a = a:

example : 2 + 3 = 5 := rfl
example (f : α → β) (a : α) : (fun x => f x) a = f a := rfl

Symmetry and Transitivity:

Eq.symm (h : a = b) : b = a
Eq.trans (h1 : a = b) (h2 : b = c) : a = c

-- Dot notation
h.symm : b = a

Substitution

Replace equals with equals:

-- Triangle notation (▸)
example (h : a = b) (hp : p a) : p b := h ▸ hp

-- Eq.subst
example (h : a = b) (hp : p a) : p b := Eq.subst h hp

Direction: h : a = b replaces a with b

Calculational Proofs (calc)

Chain equalities:

example (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d :=
  calc a = b := h1
    _ = c := h2
    _ = d := h3

-- With rewrites
example (h : a = b + 1) : a + c = b + 1 + c :=
  calc a + c = (b + 1) + c := by rw [h]
    _ = b + 1 + c := rfl

Placeholder _: Previous right-hand side.

Congruence

Equality through functions:

congrArg (f : α → β) (h : a = b) : f a = f b
congrFun (h : f = g) (a : α) : f a = g a
congr (hf : f = g) (ha : a = b) : f a = g b

Quick Reference

Need	Use
Prove `∀ x, p x`	`intro x` then prove `p x`
Use `h : ∀ x, p x`	Apply: `h t` gives `p t`
Prove `∃ x, p x`	`use w` with witness
Use `h : ∃ x, p x`	`obtain ⟨w, hw⟩ := h`
Prove `a = a`	`rfl`
Reverse equality	`h.symm`
Chain equalities	`calc`
Substitute in goal	`rw [h]`
Substitute in hyp	`h ▸ hp`

Common Mistakes

Wrong substitution direction:

-- h : a = b, goal: p b, have: hp : p a
example (h : a = b) (hp : p a) : p b := h ▸ hp  -- ✓

-- h : a = b, goal: p a, have: hp : p b
example (h : a = b) (hp : p b) : p a := h.symm ▸ hp  -- Need symm!

Forgetting rfl works with computation:

-- ❌ Too complex
example : 2 + 3 = 5 := by omega

-- ✓ Just use rfl (computes to same value)
example : 2 + 3 = 5 := rfl