Theorem: Option.orElse_assoc (GMLInit/Data/Option.lean)

State before:
α : Type u_1
x y z : Option α
⊢ (HOrElse.hOrElse (HOrElse.hOrElse x fun x => y) fun x => z) = HOrElse.hOrElse x fun x => HOrElse.hOrElse y fun x => z
Tactic:
cases x <;> cases y <;> cases z <;> rfl
State after:
no goals