x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
⊢ a ≤ sSup s ↔ ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
rw [le_iff_forall_pos_lt_add]
case refine'_1
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x, x ∈ s ∧ a + ε < x

case refine'_2
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
refine' ⟨fun H ε ε_neg => _, fun H ε ε_pos => _⟩
no goals
case refine'_1
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x, x ∈ s ∧ a + ε < x
exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))
case refine'_2.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε
case refine'_2
x y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
no goals
case refine'_2.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddAbove s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), ε < 0 → ∃ x, x ∈ s ∧ a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε
exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)