2.20 Using Assumptions Effectively

An assumption is a local term that Lean may use to solve the current goal or produce another proof. In simple proofs, assumptions are often the whole proof. In larger proofs, the main work is to recognize which assumption should be applied, destructured, rewritten, or contradicted.

Problem

You have several hypotheses in the local context, and you need to decide how to use them.

A typical context may look like this:

P Q R : Prop
hp : P
hPQ : P -> Q
hQR : Q -> R
⊢ R

The goal is R. No hypothesis has type R directly, but the context contains a path from P to R.

Solution

Use assumptions according to their type.

theorem use_assumptions_chain
    (P Q R : Prop)
    (hp : P)
    (hPQ : P -> Q)
    (hQR : Q -> R) :
    R := by
  have hq : Q := hPQ hp
  exact hQR hq

The assumption hp proves P. The assumption hPQ turns P into Q. The assumption hQR turns Q into R.

Direct Assumptions

If an assumption has exactly the target type, use exact.

theorem exact_assumption
    (P : Prop)
    (hp : P) :
    P := by
  exact hp

Lean also has the tactic assumption.

theorem assumption_tactic
    (P : Prop)
    (hp : P) :
    P := by
  assumption

The tactic searches the local context for a hypothesis whose type matches the goal.

Applying Implication Assumptions

If an assumption is an implication, apply it to a proof of its premise.

theorem apply_implication_assumption
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp

You can also use apply backward.

theorem apply_backward_assumption
    (P Q : Prop)
    (hp : P)
    (hPQ : P -> Q) :
    Q := by
  apply hPQ
  exact hp

After apply hPQ, the goal changes from Q to P.

Destructuring Conjunction Assumptions

A conjunction assumption contains two proofs.

theorem use_and_assumption
    (P Q : Prop)
    (h : P ∧ Q) :
    Q ∧ P := by
  exact ⟨h.right, h.left⟩

For longer proofs, destructure it first.

theorem use_and_assumption_rcases
    (P Q : Prop)
    (h : P ∧ Q) :
    Q ∧ P := by
  rcases h with ⟨hp, hq⟩
  exact ⟨hq, hp⟩

This makes the context easier to read.

Splitting Disjunction Assumptions

A disjunction assumption must be handled by cases.

theorem use_or_assumption
    (P Q R : Prop)
    (h : P ∨ Q)
    (hPR : P -> R)
    (hQR : Q -> R) :
    R := by
  cases h with
  | inl hp =>
    exact hPR hp
  | inr hq =>
    exact hQR hq

A disjunction does not give both sides. It gives one side in each branch.

Using Negated Assumptions

A negated assumption is a function into False.

theorem use_not_assumption
    (P R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    R := by
  have hf : False := hnp hp
  cases hf

The direct form is:

theorem use_not_assumption_direct
    (P R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    R := by
  exact False.elim (hnp hp)

Use this when contradiction is immediate.

Using Equality Assumptions

An equality assumption rewrites the goal or another hypothesis.

theorem use_eq_assumption
    (a b : Nat)
    (hAB : a = b) :
    a + 1 = b + 1 := by
  rw [hAB]

Rewrite in a hypothesis when the useful fact has the wrong shape.

theorem use_eq_in_hypothesis
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  rw [hAB] at ha
  exact ha

Using Universal Assumptions

A universal assumption is a function. Apply it to a value.

theorem use_forall_assumption
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (h : ∀ x : α, P x) :
    P a := by
  exact h a

For multiple quantifiers, apply arguments in order.

theorem use_forall_two
    (α : Type)
    (P : α -> α -> Prop)
    (a b : α)
    (h : ∀ x y : α, P x y) :
    P a b := by
  exact h a b

Using Existential Assumptions

An existential assumption contains a hidden witness. Unpack it.

theorem use_exists_assumption
    (P : Nat -> Prop)
    (h : ∃ n : Nat, P n) :
    ∃ m : Nat, P m := by
  rcases h with ⟨n, hn⟩
  use n
  exact hn

After destructuring, the witness and its proof become ordinary assumptions.

Combining Assumption Types

Real proofs often combine several kinds of assumptions.

theorem combined_assumption_use
    (P Q R S : Prop)
    (h : P ∧ Q)
    (hQR : Q -> R)
    (hRS : R -> S) :
    P ∧ S := by
  rcases h with ⟨hp, hq⟩
  have hr : R := hQR hq
  have hs : S := hRS hr
  exact ⟨hp, hs⟩

The proof first extracts useful assumptions, then applies implications, then constructs the final conjunction.

The assumption Tactic

The tactic assumption solves a goal if the exact proposition is already present.

theorem assumption_exact
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P := by
  assumption

It does not apply implications automatically.

-- This does not work:
-- theorem assumption_not_enough
--     (P Q : Prop)
--     (hp : P)
--     (hPQ : P -> Q) :
--     Q := by
--   assumption

Here no assumption has type Q. You must apply hPQ to hp.

The first | assumption Pattern

In larger tactic scripts, you may use first to try simple assumptions before other tactics.

theorem first_assumption_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · first | assumption | exact hp
  · first | assumption | exact hq

This is rarely needed in beginner proofs. It becomes useful when writing reusable tactic scripts.

Avoiding Assumption Ambiguity

When several assumptions have similar types, use explicit names.

theorem explicit_assumption_choice
    (P Q : Prop)
    (hp₁ : P)
    (hp₂ : P)
    (hPQ : P -> Q) :
    Q := by
  exact hPQ hp₁

Both hp₁ and hp₂ prove P, so either works. Choosing explicitly makes the proof deterministic and readable.

Common Patterns

Use a direct hypothesis:

exact hp

Search for a direct hypothesis:

assumption

Apply an implication:

exact hPQ hp

Destructure conjunction:

rcases h with ⟨hp, hq⟩

Split disjunction:

cases h with
| inl hp => ...
| inr hq => ...

Use contradiction:

exact False.elim (hnp hp)

Rewrite with equality:

rw [hAB]

Apply universal hypothesis:

exact h a

Unpack existential:

rcases h with ⟨x, hx⟩

Common Pitfalls

Do not expect assumption to apply implications or destructure hypotheses.

Do not use a disjunction assumption as if both sides were available.

Do not leave useful information hidden inside a conjunction or existential when the proof needs its components.

Do not rewrite with an equality before checking its direction.

Do not rely on generic names when several assumptions have similar types.

Takeaway

An assumption is useful according to its type. Direct assumptions solve goals, implications are applied, conjunctions are projected, disjunctions are split, negations produce contradictions, equalities rewrite, universals are applied to values, and existentials are unpacked. Reading the type of each assumption determines the next proof move.