Lean Proof Mental Model Part 1

1. Core Idea

proposition = type
proof = value
theorem proving = constructing a value of a type
tactics = a guided way to construct the proof value step by step

Example:

-- term proof
example (P : Prop) : P -> P :=
  fun h => h

-- tactic proof
example (P : Prop) : P -> P := by
  intro h
  exact h

2. Two Directions Model

Goal → BUILD. It is like the return type of a function, so I need to build a value of that type.
Hypothesis → USE / OPEN. These are inputs I can assume are already available, so I can use them to build the goal. Even an “input” can appear inside the goal. For example, if the goal is A -> B, then intro hA gives me hA : A.

With that mindset, choose tactics based on whether the structure appears in the goal or in the hypotheses.

Structure	As Goal	As Hypothesis
`A → B`	intro	apply/use it
`P ∧ Q`	constructor	cases
`P ∨ Q`	left / right	cases
`∃ x, P x`	use	cases
`∀ x, P x`	intro x	h t (`h : ∀ x, P x`)
`a = b`	`rw / rfl`	`rw [h]` (`h: a=b`)

3. Why intro Works

When the goal is:

⊢ A -> B

Lean is asking me to build a function:

proof of A -> proof of B

So intro hA means: suppose somebody gives me a proof of A. It does not assert A globally; it introduces a hypothetical parameter.

Term proof:

example (A B : Prop) (h : A -> B) : A -> B :=
  fun hA => h hA

Tactic proof:

example (A B : Prop) (h : A -> B) : A -> B := by
  intro hA
  exact h hA

4. Categories of Reasoning

These are not strict mathematical categories. They are recurring proof problem patterns.

4.1. 1. Logic (structure)

Forms: →, ∧, ∨, ¬
Goal: construct
Hypothesis: open / decompose

Examples:

-- → as goal: introduce input, then build output
example (A B : Prop) (h : A -> B) : A -> B := by
  intro ha
  exact h ha

-- → as hypothesis: apply/use it
example (A B : Prop) (h : A -> B) (ha : A) : B := by
  exact h ha

-- ∧ as goal: build both sides
example (A B : Prop) (ha : A) (hb : B) : A ∧ B := by
  constructor
  · exact ha
  · exact hb

-- ∧ as hypothesis: open/decompose it
example (A B : Prop) (h : A ∧ B) : A := by
  cases h with
  | intro ha hb => exact ha

-- ∨ as goal: choose left or right
example (A B : Prop) (ha : A) : A ∨ B := by
  left
  exact ha
example (A B : Prop) (hb : B) : A ∨ B := by
  right
  exact hb

-- ∨ as hypothesis: split into branches
example (A B C : Prop) (h : A ∨ B) (ha : A -> C) (hb : B -> C) : C := by
  cases h with
  | inl a => exact ha a
  | inr b => exact hb b

-- ¬ as goal: assume the proposition, derive contradiction
example (A : Prop) (h : A -> False) : ¬ A := by
  intro ha
  exact h ha

-- ¬ as hypothesis: use it as A -> False
example (A : Prop) (hnot : ¬ A) (ha : A) : False := by
  exact hnot ha

4.2. 2. Equality (rewriting)

Form: =
rw: rewrite using equality
rfl: finish when both sides are identical

Examples:

-- = as goal: close when both sides reduce to the same expression
example : 1 + 1 = 2 := by
  rfl

-- = as hypothesis: rewrite with it
example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]

4.3. 3. Data / Structure

Types: Nat, List, etc.
cases: split by structure
induction: recursive reasoning

Examples:

-- cases on Nat: zero case and successor case
example (n : Nat) : n = 0 ∨ ∃ m : Nat, n = m + 1 := by
  cases n with
  | zero =>
      left
      rfl
  | succ m =>
      right
      exact ⟨m, rfl⟩

-- induction on Nat: prove base case and recursive step
example (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp

4.4. 4. Computation / Simplification

Lean reduces expressions automatically
Tools: rfl, simp
Example: 1 + 1 = 2

Examples:

-- rfl works when computation makes both sides identical
example : (fun x : Nat => x + 1) 2 = 3 := by
  rfl

-- simp proves goals by simplifying known definitions/rules
example (xs : List Nat) : [] ++ xs = xs := by
  simp

4.5. 5. Quantifiers

Forms: ∀, ∃

Form	Goal Action	Hypothesis Action
∀	intro	apply (h x)
∃	use	cases

Examples:

-- ∀ as goal: introduce an arbitrary x
example : ∀ n : Nat, n = n := by
  intro n
  rfl

-- ∀ as hypothesis: apply it to a concrete value
example (P : Nat -> Prop) (h : ∀ n : Nat, P n) : P 3 := by
  exact h 3

-- ∃ as goal: provide a witness and prove the property
example : ∃ n : Nat, n = 3 := by
  exact ⟨3, rfl⟩

-- ∃ as hypothesis: open it into witness + proof
example (P : Nat -> Prop) (h : ∃ n : Nat, P n) : ∃ n : Nat, P n := by
  cases h with
  | intro n hn =>
      exact ⟨n, hn⟩

4.6. 6. Classical reasoning

by_cases, contradiction, etc.

4.7. 7. Automation / search

simp, aesop, etc.

5. Important Quiz Patterns

5.1. Implication chaining

example (P Q R : Prop) :
    (P -> Q) -> (Q -> R) -> P -> R := by
  intro hpq
  intro hqr
  intro hp
  exact hqr (hpq hp)

5.2. Negation

¬P means P -> False

example (P Q : Prop) :
    (P -> Q) -> ¬ Q -> ¬ P := by
  intro hpq
  intro hnq
  intro hp
  exact hnq (hpq hp)

5.3. OR branching

example (P Q R : Prop) :
    (P -> R) -> (Q -> R) -> (P ∨ Q) -> R := by
  intro hpr
  intro hqr
  intro hpq
  cases hpq with
  | inl hp =>
      exact hpr hp
  | inr hq =>
      exact hqr hq

5.4. AND + OR decomposition

example (P Q R : Prop) :
    P ∧ (Q ∨ R) -> (P ∧ Q) ∨ (P ∧ R) := by
  intro h
  cases h with
  | intro hp hqr =>
      cases hqr with
      | inl hq =>
          left
          constructor
          · exact hp
          · exact hq
      | inr hr =>
          right
          constructor
          · exact hp
          · exact hr

5.5. Existential witness construction

Equations often tell you the witness directly.
In Mathlib-oriented tactic style this is often written with use.
In bare Lean, the explicit constructor form ⟨witness, proof⟩ verifies without extra imports.

example (x : Nat) : ∃ y, y = x + 1 := by
  exact ⟨x + 1, rfl⟩

6. Tactical Interpretation (Programming View)

Tactic	Programming Interpretation
intro	function argument
intros	introduce multiple function arguments
cases	pattern match
induction	recursive pattern match
use	construct existential witness
constructor	build pair / struct fields
left/right	choose union branch
exact	return value
apply	call function backward from goal
have	local let-binding / intermediate value
specialize	call a universal hypothesis with arguments
rw	substitution
simp	simplify / normalize
rfl	trivial equality
assumption	return matching value from context
contradiction	close impossible branch
by_cases	branch on a proposition

7. Follow up

Study Classical reasoning and Automation / search
Learn how much custom tactic code is useful in practice

8. Appendix: My First Step Toward Understanding Tactic Proofs

example (P Q R : Prop) :
  (P ∨ Q) ∧ (P → R) ∧ (Q → R) → R := by
  -- ?

I think I can now understand this kind of proof quiz. No matter which similar quiz I see, I can first read it as a mathematical description. The important part is understanding the concept; choosing the exact tactic is more like an implementation detail.

For this specific quiz, we can use cases to open the hypothesis. That gives us sub-hypotheses to work with. For example, if one hypothesis has the shape P ∨ Q, we split it into two branches. In the first branch we get a proof of P, and in the second branch we get a proof of Q. Then we can apply the corresponding hypotheses, such as P -> R or Q -> R, to produce R in each branch.