α : Type ?u.217125
β : Type ?u.217128
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b
α : Type ?u.217125
β : Type ?u.217128
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p
rintro b rfl
case h
α : Type ?u.217125
β : Type ?u.217128
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b
α : Type ?u.217125
β : Type ?u.217128
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b
apply NNReal.inv_le_of_le_mul
no goals
case h
α : Type ?u.217125
β : Type ?u.217128
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b
rwa [← coe_mul, ← coe_one, coe_le_coe] at hb