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