α : Type ?u.827518
β : Type ?u.827521
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (a * ⊤) = 0
α : Type ?u.827518
β : Type ?u.827521
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (⊤ * a) = 0
rw [mul_comm]
no goals
α : Type ?u.827518
β : Type ?u.827521
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (a * ⊤) = 0
exact toReal_mul_top _