cases' hnonvide with x x_in
case refine_1.left
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
hnonvide : ∃ x, x ∈ A
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
⊢ a ≤ sSup A
case refine_1.left.intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
A : Set ℝ
h : A ⊆ Icc a b
b_maj : ∀ y ∈ A, y ≤ b
Sup_maj : upper_bound A (sSup A)
x : ℝ
x_in : x ∈ A
⊢ a ≤ sSup A