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

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