x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddAbove S
⊢ IsLUB S (choose (_ : ∃ x, IsLUB S x))
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddAbove S
⊢ IsLUB S (sSup S)
simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
no goals
x y : ℝ
S : Set ℝ
h₁ : Set.Nonempty S
h₂ : BddAbove S
⊢ IsLUB S (choose (_ : ∃ x, IsLUB S x))
apply Classical.choose_spec