case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
ht : Set.Nonempty t
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
refine' hs.out c.2 B.2 ⟨_, _⟩
no goals
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)
exact (Subtype.mono_coe s).le_csSup_image hct ⟨B, hB⟩
no goals
case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
exact (Subtype.mono_coe s).csSup_image_le ⟨c, hct⟩ hB