case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ ∃ n, n > 0 ∧ (↑n)⁻¹ * a < b
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
⊢ ∃ n, n > 0 ∧ (↑n)⁻¹ * a < b
rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b
case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ ∃ n, n > 0 ∧ (↑n)⁻¹ * a < b
use n, npos
case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b
case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b
rw [← ENNReal.div_eq_inv_mul]
no goals
case intro.intro
α : Type ?u.341859
β : Type ?u.341862
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b
exact div_lt_of_lt_mul' hn