no goals
α : Type ?u.298762
β : Type ?u.298765
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ⊤
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
rw [← @ENNReal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
  one_mul]