theorem my_theorem {A B C : Prop} :
A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
assume h : A ∧ (B ∨ C),
have A, from and.left h,
have B ∨ C, from and.right h,
show (A ∧ B) ∨ (A ∧ C), from
or.elim ‹B ∨ C›
(assume : B,
have A ∧ B, from and.intro ‹A› ‹B›,
show (A ∧ B) ∨ (A ∧ C), from or.inl this)
(assume : C,
have A ∧ C, from and.intro ‹A› ‹C›,
show (A ∧ B) ∨ (A ∧ C), from or.inr this)