Use what you already know

Everything before the final colon in a statement is context. In theorem exercise (P : Prop) (h : P) : P, the context holds a proposition P and a proof h of it, and the goal is P. The panel shows P : Prop, then h : P, then ⊢ P.

In Lean a proof of P is a value whose type is P, the same way 3 is a value whose type is Nat. That is why hypotheses are named like variables and used like variables. h is not a note saying “P is true”; h is the evidence.

exact e closes the goal when e has exactly the type of the goal. When the types do not line up, Lean prints what it got and what it wanted, which is the error you will read most often.

A common slip is to write exact P. P is the proposition, not a proof of it: its type is Prop, not P. The message says so in those words, and recognising it once saves a lot of time later.

Worked example

-- Two proofs are available; the goal decides which one fits.
example (A B : Prop) (ha : A) (hb : B) : B := by
  exact hb

-- Handing Lean the proposition instead of a proof of it:
--   example (P : Prop) (h : P) : P := by exact P
--
--   Type mismatch
--     P
--   has type
--     Prop
--   of sort `Type` but is expected to have type
--     P
--   of sort `Prop`

Lean also warns that ha went unused in the first example. It keeps track of assumptions you never touch, which is a useful signal when a proof has grown longer than it should be.