α : Type ?u.127753
β : Type ?u.127756
a b c d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
α : Type ?u.127753
β : Type ?u.127756
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b
refine' ⟨fun hab => _, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
case intro.intro
α : Type ?u.127753
β : Type ?u.127756
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
α : Type ?u.127753
β : Type ?u.127756
a b c d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
case intro.intro
α : Type ?u.127753
β : Type ?u.127756
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
lift a to ℝ≥0 using ac.ne_top
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
rw [coe_lt_coe] at ac
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
no goals
case intro.intro.intro
α : Type ?u.127753
β : Type ?u.127756
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b
rwa [← coe_add, add_tsub_cancel_of_le ac.le]