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

State before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min x ↑y) = min (untop' y x) y
Tactic:
rw [min_comm x, min_comm _ y]
State after:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min (↑y) x) = min y (untop' y x)

State before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min (↑y) x) = min y (untop' y x)
Tactic:
apply untop'_min_left
State after:
no goals