no goals
α : Type ?u.299453
β : Type ?u.299456
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b : ℝ≥0∞
r : ℝ≥0
hr₀ : r ≠ 0
⊢ a ≤ r⁻¹ • b ↔ r • a ≤ b
simpa [hr₀, ENNReal.smul_def] using (mul_le_iff_le_inv (coe_ne_zero.mpr hr₀) coe_ne_top).symm