s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ sSup s = ↑(greatestOfBdd b Hb Hinh)
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
⊢ sSup s = ↑(greatestOfBdd b Hb Hinh)
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s)) =
    ↑(greatestOfBdd b Hb Hinh)
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ sSup s = ↑(greatestOfBdd b Hb Hinh)
simp only [sSup, this, and_self, dite_true]
no goals
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ (z : ℤ), z ∈ s → z ≤ b
Hinh : ∃ z, z ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s)) =
    ↑(greatestOfBdd b Hb Hinh)
convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm