Practice: transform both sides | Your first Lean proofs

This checkpoint composes the moves from the course. The outer implication asks you to introduce a conjunction, opening it gives two assumptions, and the conjunctive target asks for two separate proofs.

Each branch has its own implication to work backwards through, and the assumptions you unpacked at the start close the goals that remain.

There is no step checklist here. Build the proof from the changing goal state, and use the hints only when you need the next structural move. The further exercises are harder and have fewer hints; plan them with sorry if that helps.

Worked example

example (A B C : Prop) (left : A → B) (right : A → C) : A → B ∧ C := by
  intro ha
  constructor
  · apply left
    exact ha
  · apply right
    exact ha

The example sends one assumption through two functions. Your exercise first opens a pair, then sends each component through its matching function.

Takeaway

Longer proofs are compositions of local moves: introduce, unpack, split, work backwards and close each resulting goal with the matching evidence.

Exercise 1 of 3

Transform both sides of P ∧ Q: use f : P → R for the left result and g : Q → S for the right result.

Exercise.lean

1theorem exercise (P Q R S : Prop) (f : P → R) (g : Q → S) : P ∧ Q → R ∧ S := by

given

Loading editor…

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

P Q R S:Prop

f:P → R

g:Q → S

⊢P ∧ Q → R ∧ S

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check