Theorem: WithTop.untop'_min_left (One.lean)

State before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : α
y : WithTop α
⊢ untop' d (min (↑x) y) = min x (untop' x y)
Tactic:
cases y with
| none => simp only [none_eq_top, ge_iff_le, le_top, min_eq_left, untop'_coe, untop'_top, min_self]
| some y' => rw [some_eq_coe, ← coe_min, untop'_coe, untop'_coe]
State after:
no goals

State before:
case none
α : Type u_1
d : α
inst✝ : LinearOrder α
x : α
⊢ untop' d (min (↑x) none) = min x (untop' x none)
Tactic:
simp only [none_eq_top, ge_iff_le, le_top, min_eq_left, untop'_coe, untop'_top, min_self]
State after:
no goals

State before:
case some
α : Type u_1
d : α
inst✝ : LinearOrder α
x y' : α
⊢ untop' d (min (↑x) (Option.some y')) = min x (untop' x (Option.some y'))
Tactic:
rw [some_eq_coe, ← coe_min, untop'_coe, untop'_coe]
State after:
no goals