case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s = ↑(greatestOfBdd (choose h2) (_ : choose h2 ∈ upperBounds s) h1)
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s ∈ s
convert (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
no goals
case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s = ↑(greatestOfBdd (choose h2) (_ : choose h2 ∈ upperBounds s) h1)
exact dif_pos ⟨h1, h2⟩