simple proof in Lean and show_term

simple.lean

import tactic

example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
begin 
 show_term { 
 intro h,
 have ha  := h.left,
 have hbc := h.right,
 cases hbc with hb hc,
 exact or.inl (and.intro ha hb),
 exact or.inr (and.intro ha hc), },
end

example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
begin 
 show_term { 
 intro h,
 have ha  := h.left,
 have hbc := h.right,
 cases hbc with hb hc,
 left,
 exact and.intro ha hb,
 right,
 exact and.intro ha hc, },
end

example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := 
 λ h, h.right.dcases_on (λ (hb : B), or.inl ⟨h.left, hb⟩) (λ (hc : C), or.inr ⟨h.left, hc⟩)

example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := 
 λ h, or.elim h.right 
   (λ hb, or.inl $ and.intro h.1 hb) 
   (λ hc, or.inr $ and.intro h.1 hc)