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