refine ⟨sSup A, ?_, ?_⟩
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)
⊢ ∃ x ∈ Icc a b, is_sup A x
case refine_1
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)
⊢ sSup A ∈ Icc a b

case refine_2
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)
⊢ is_sup A (sSup A)