α : Type ?u.86061
β : Type ?u.86064
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤
α : Type ?u.86061
β : Type ?u.86064
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ⊤ = if c = 0 then 0 else ⊤
rw [← smul_one_mul, mul_top']
no goals
α : Type ?u.86061
β : Type ?u.86064
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤
simp_rw [smul_eq_zero, or_iff_left (one_ne_zero' ℝ≥0∞)]