[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), BddAbove s → a ∈ s → a ≤ sSup s
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
⊢ n ≤ sSup s
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s :=
  ⟨⟨n, hns⟩, hs⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ n ≤ sSup s
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddAbove s
hns : n ∈ s
this : Set.Nonempty s ∧ BddAbove s
⊢ n ≤ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s))
[PROOFSTEP]
exact (greatestOfBdd _ _ _).2.2 n hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ a
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
⊢ sSup s ≤ n
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s :=
  ⟨hs, ⟨n, hns⟩⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
this : Set.Nonempty s ∧ BddAbove s
⊢ sSup s ≤ n
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ upperBounds s
this : Set.Nonempty s ∧ BddAbove s
⊢ ↑(greatestOfBdd (choose (_ : BddAbove s)) (_ : choose (_ : BddAbove s) ∈ upperBounds s) (_ : Set.Nonempty s)) ≤ n
[PROOFSTEP]
exact hns (greatestOfBdd _ (Classical.choose_spec this.2) _).2.1
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), BddBelow s → a ∈ s → sInf s ≤ a
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
⊢ sInf s ≤ n
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s :=
  ⟨⟨n, hns⟩, hs⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ sInf s ≤ n
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : BddBelow s
hns : n ∈ s
this : Set.Nonempty s ∧ BddBelow s
⊢ ↑(leastOfBdd (choose (_ : BddBelow s)) (_ : choose (_ : BddBelow s) ∈ lowerBounds s) (_ : Set.Nonempty s)) ≤ n
[PROOFSTEP]
exact (leastOfBdd _ _ _).2.2 n hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
⊢ ∀ (s : Set ℤ) (a : ℤ), Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf s
[PROOFSTEP]
intro s n hs hns
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
⊢ n ≤ sInf s
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s :=
  ⟨hs, ⟨n, hns⟩⟩
    -- Porting note: this was `rw [dif_pos this]`
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
this : Set.Nonempty s ∧ BddBelow s
⊢ n ≤ sInf s
[PROOFSTEP]
simp only [this, and_self, dite_true, ge_iff_le]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
n : ℤ
hs : Set.Nonempty s
hns : n ∈ lowerBounds s
this : Set.Nonempty s ∧ BddBelow s
⊢ n ≤ ↑(leastOfBdd (choose (_ : BddBelow s)) (_ : choose (_ : BddBelow s) ∈ lowerBounds s) (_ : Set.Nonempty s))
[PROOFSTEP]
exact hns (leastOfBdd _ (Classical.choose_spec this.2) _).2.1
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
hs : ¬BddAbove s
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
simp [hs]
[GOAL]
src✝¹ : LinearOrderedCommRing ℤ := linearOrderedCommRing
src✝ : Lattice ℤ := LinearOrder.toLattice
s : Set ℤ
hs : ¬BddBelow s
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
simp [hs]
[GOAL]
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)
[PROOFSTEP]
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
[GOAL]
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)
[PROOFSTEP]
simp only [sSup, this, and_self, dite_true]
[GOAL]
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)
[PROOFSTEP]
convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm
[GOAL]
⊢ ¬(Set.Nonempty ∅ ∧ BddAbove ∅)
[PROOFSTEP]
simp
[GOAL]
s : Set ℤ
h : ¬BddAbove s
⊢ ¬(Set.Nonempty s ∧ BddAbove s)
[PROOFSTEP]
simp [h]
[GOAL]
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)
[PROOFSTEP]
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
[GOAL]
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)
[PROOFSTEP]
simp only [sInf, this, and_self, dite_true]
[GOAL]
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)
[PROOFSTEP]
convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm
[GOAL]
⊢ ¬(Set.Nonempty ∅ ∧ BddBelow ∅)
[PROOFSTEP]
simp
[GOAL]
s : Set ℤ
h : ¬BddBelow s
⊢ ¬(Set.Nonempty s ∧ BddBelow s)
[PROOFSTEP]
simp [h]
[GOAL]
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s ∈ s
[PROOFSTEP]
convert (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
[GOAL]
case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddAbove s
⊢ sSup s = ↑(greatestOfBdd (choose h2) (_ : choose h2 ∈ upperBounds s) h1)
[PROOFSTEP]
exact dif_pos ⟨h1, h2⟩
[GOAL]
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddBelow s
⊢ sInf s ∈ s
[PROOFSTEP]
convert (leastOfBdd _ (Classical.choose_spec h2) h1).2.1
[GOAL]
case h.e'_4
s : Set ℤ
h1 : Set.Nonempty s
h2 : BddBelow s
⊢ sInf s = ↑(leastOfBdd (choose h2) (_ : choose h2 ∈ lowerBounds s) h1)
[PROOFSTEP]
exact dif_pos ⟨h1, h2⟩
