I’ve typed the following into Lean4 in VSCode:

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) :=
begin

and it tells me “unknown identifier ‘begin'”. When I type the end two lines down, it tells me “invalid ‘end’, insufficient scopes”. What am I doing wrong? Did I not set Lean up properly?