case intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
α : Type ?u.125408
β : Type ?u.125411
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b
⊢ ∃ q, 0 ≤ q ∧ a < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
case intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c✝ d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
case intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
rcases exists_between h with ⟨c, pc, cb⟩
case intro.intro.intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r✝ p✝ q p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
case intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c✝ d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r✝ p✝ q✝ p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < Real.toNNReal ↑q
qr : Real.toNNReal ↑q < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
case intro.intro.intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r✝ p✝ q p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.125408
β : Type ?u.125411
b c d : ℝ≥0∞
r✝ p✝ q✝ p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < Real.toNNReal ↑q
qr : Real.toNNReal ↑q < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩