Review: choose the next move | Your first Lean proofs

This lesson has no new material and no step checklists. Each exercise mixes moves from the whole course: introducing, unpacking, splitting, applying, naming intermediate facts, rewriting and splitting a Boolean.

Before you type anything, read the goal and the context and decide which move the goal asks for. A goal with → wants intro. A goal with ∧ wants a split or a pair. A hypothesis with ∧ wants to be opened. An equation in the context is a license to rewrite.

Plan with sorry if the proof has more than one branch. The hints only name a direction; the full answer stays behind Reveal a solution.

Worked example

-- A different goal, solved by reading its shape:
example (A B C : Prop) (hab : A → B) (h : A ∧ C) : C ∧ B := by
  obtain ⟨ha, hc⟩ := h   -- a pair in the context: open it
  constructor            -- a pair as the goal: split it
  · exact hc
  · exact hab ha

The comments name the reason for each move. Try to say the same reasons to yourself as you solve the exercises.

Takeaway

Reading the outermost shape of the goal and of each hypothesis tells you the next move. The next course adds the connectives this one left out: or, not and if-and-only-if.

Exercise 1 of 4

Prove Q ∧ R from an implication and a pair.

Exercise.lean

1theorem exercise (P Q R : Prop) (hpq : P → Q) (h : P ∧ R) : Q ∧ R := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P Q R:Prop

hpq:P → Q

h:P ∧ R

⊢Q ∧ R

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check