case inl

⊢ ↑(⊤ * ↑0) = ⊤ * ↑↑0

case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
x : ℝ≥0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
rcases eq_or_ne x 0 with (rfl | h0)
no goals
case inl

⊢ ↑(⊤ * ↑0) = ⊤ * ↑↑0
simp
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑⊤ = ⊤ * ↑↑x
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]
no goals
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑⊤ = ⊤ * ↑↑x
exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt