obtain hlt | hle := lt_or_le a w₀
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ a ∈ S
case inl
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hlt : a < w₀
⊢ a ∈ S

case inr
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hle : w₀ ≤ a
⊢ a ∈ S