[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
let ⟨b, Hb⟩ := Hbdd
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
exact ⟨lb, H⟩
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(leastOfBdd b Hb Hinh) = ↑(leastOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
[GOAL]
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } = ↑(leastOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
[GOAL]
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → n' ≤ z
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } =
    ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → n' ≤ z) }
[PROOFSTEP]
exact le_antisymm (h2n _ hn') (h2n' _ hn)
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)
[PROOFSTEP]
rw [neg_neg]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt
[PROOFSTEP]
exact Helt
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P (- -z)
[PROOFSTEP]
rwa [neg_neg]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
let ⟨b, Hb⟩ := Hbdd
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
exact ⟨lb, H⟩
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(greatestOfBdd b Hb Hinh) = ↑(greatestOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
[GOAL]
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } = ↑(greatestOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
[GOAL]
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → z ≤ n'
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } =
    ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → z ≤ n') }
[PROOFSTEP]
exact le_antisymm (h2n' _ hn) (h2n _ hn')
