Module 3 · Lesson 1

intro — Introducing Assumptions

intro moves things from the goal into your hypotheses. It's how you assume things to prove implications and universals.

Proving Implications

When your goal is P → Q, use introto assume P and prove Q:

lean

1example : True → True := by
2  intro h
3  -- Before: ⊢ True → True
4  -- After:  h : True ⊢ True
5  trivial
6
7example (P : Prop) : P → P := by
8  intro hp
9  -- hp : P ⊢ P
10  exact hp

Logically, to prove "if P then Q," you assume P and derive Q.

Proving Universals

When your goal is ∀ x, P x, use introto introduce an arbitrary x:

lean

1example : ∀ n : Nat, n = n := by
2  intro n
3  -- Before: ⊢ ∀ n : Nat, n = n
4  -- After:  n : Nat ⊢ n = n
5  rfl
6
7example : ∀ a b : Nat, a + b = b + a := by
8  intro a b
9  -- a b : Nat ⊢ a + b = b + a
10  exact Nat.add_comm a b

Key Takeaway

intro x says "let x be arbitrary" for universals, or "assume x" for implications. The goal changes, and x becomes a hypothesis.

Introducing Multiple Things

lean

1-- Introduce several at once
2example : ∀ a b c : Nat, a + b + c = c + b + a := by
3  intro a b c
4  ring
5
6-- Mix of universals and implications
7example : ∀ (P Q : Prop), P → Q → P := by
8  intro P Q hp hq
9  -- P Q : Prop, hp : P, hq : Q ⊢ P
10  exact hp
11
12-- Alternative: use multiple intro calls
13example : ∀ (n : Nat), n > 0 → n ≥ 1 := by
14  intro n
15  intro h
16  omega

Naming Conventions

lean

1-- Common patterns:
2-- h, h1, h2 for hypotheses (proof terms)
3-- hp, hq for proofs of P, Q
4-- n, m, k for numbers
5-- a, b, c for arbitrary values
6-- x, y, z for elements
7-- xs, ys for lists
8-- f, g for functions
9
10example (P Q R : Prop) : P → Q → R → P := by
11  intro hp hq hr
12  exact hp

intro with Patterns

You can destructure as you introduce:

lean

1-- Introduce and destructure a conjunction
2example (P Q : Prop) : P ∧ Q → Q ∧ P := by
3  intro ⟨hp, hq⟩
4  -- Instead of: intro h; obtain ⟨hp, hq⟩ := h
5  exact ⟨hq, hp⟩
6
7-- Works with existentials too
8example : (∃ n : Nat, n > 5) → ∃ n : Nat, n > 0 := by
9  intro ⟨n, hn⟩
10  -- n : Nat, hn : n > 5
11  exact ⟨n, by omega⟩

intros: Introduce All

lean

1-- intros introduces everything it can
2example : ∀ a b : Nat, a = b → b = a := by
3  intros
4  -- Introduces a, b, and the equality proof with auto-generated names
5  assumption
6
7-- Better to name them explicitly:
8example : ∀ a b : Nat, a = b → b = a := by
9  intro a b hab
10  exact hab.symm

⚠

intros auto-generates names like a✝, which can be confusing. Prefer explicit intro a b cwhen possible.

Common Mistakes

Mistake 1: Forgetting intro when needed

lean

1-- ❌ Won't work: can't prove P → Q directly
2-- example (P Q : Prop) (hq : Q) : P → Q := by
3--   exact hq  -- Error: expected P → Q, got Q
4
5-- ✓ Correct: intro first, then provide Q
6example (P Q : Prop) (hq : Q) : P → Q := by
7  intro hp
8  exact hq

Mistake 2: Wrong number of intros

lean

1-- Be careful with nested implications
2example : ∀ n : Nat, n > 0 → n ≠ 0 := by
3  intro n hn  -- Need TWO intros: one for n, one for the hypothesis
4  omega
5
6-- If you only do one intro:
7-- intro n would leave goal: n > 0 → n ≠ 0

Mistake 3: Introducing when you should apply

lean

1-- If the goal is not an implication or forall, intro won't work
2example (P : Prop) (hp : P) : P := by
3  -- intro h  -- ❌ Error: P is not a function type
4  exact hp  -- ✓ Correct

Exercise 1: Introduce and Use

Use intro to bring assumptions into context and finish the proof.

lean

1example (P Q : Prop) : P → Q → Q := by
2  intro hp hq
3  exact hq

Exercise 2: Universal Statement

Introduce the universal variable and prove reflexivity.

lean

1example : ∀ n : Nat, n + 0 = n := by
2  intro n
3  simp

Exercise 3: Pattern Intro

Use pattern matching in intro to destructure the conjunction.

lean

1example (P Q : Prop) : P ∧ Q → Q ∧ P := by
2  intro ⟨hp, hq⟩
3  exact ⟨hq, hp⟩

Function Goals

Remember: P → Q is a function type. introis like writing fun hp => ...:

lean

1-- These are equivalent:
2example : Nat → Nat := fun n => n + 1
3example : Nat → Nat := by intro n; exact n + 1
4
5-- For propositions:
6example (P Q : Prop) (f : P → Q) (hp : P) : Q := by
7  apply f
8  exact hp
9
10-- Or more directly:
11example (P Q : Prop) (f : P → Q) (hp : P) : Q := f hp

Deep Dive: intro and Lambda

Under the hood, intro x constructs a lambda:

lean

1-- These produce the same proof term:
2theorem t1 : ∀ n : Nat, n = n := by intro n; rfl
3theorem t2 : ∀ n : Nat, n = n := fun n => rfl
4
5#print t1  -- fun n => rfl
6#print t2  -- fun n => rfl

Tactics are just a convenient way to build proof terms. You can always see what term was built using #print.

Examples

Implication Chain

lean

1example (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
2  intro hpq hqr hp
3  -- hpq : P → Q
4  -- hqr : Q → R
5  -- hp : P
6  -- ⊢ R
7  apply hqr
8  apply hpq
9  exact hp

Universal with Hypothesis

lean

1example : ∀ n : Nat, n > 0 → n ≠ 0 := by
2  intro n hn
3  -- n : Nat
4  -- hn : n > 0
5  -- ⊢ n ≠ 0
6  omega

Nested Universals

lean

1example : ∀ (f : Nat → Nat), (∀ n, f n = n) → f 5 = 5 := by
2  intro f hf
3  -- f : Nat → Nat
4  -- hf : ∀ n, f n = n
5  -- ⊢ f 5 = 5
6  exact hf 5

exact & apply Next: have & let