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

State before:
α : Type u_1
x : Option α
⊢ (HOrElse.hOrElse none fun x_1 => x) = x
Tactic:
rfl
State after:
no goals