/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Mario Carneiro

! This file was ported from Lean 3 source module data.int.least_greatest
! leanprover-community/mathlib commit 3342d1b2178381196f818146ff79bc0e7ccd9e2d
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Order.Basic

/-! # Least upper bound and greatest lower bound properties for integers

In this file we prove that a bounded above nonempty set of integers has the greatest element, and a
counterpart of this statement for the least element.

## Main definitions

* `Int.leastOfBdd`: if `P : ℤ → Prop` is a decidable predicate, `b` is a lower bound of the set
  `{m | P m}`, and there exists `m : ℤ` such that `P m` (this time, no witness is required), then
  `Int.leastOfBdd` returns the least number `m` such that `P m`, together with proofs of `P m` and
  of the minimality. This definition is computable and does not rely on the axiom of choice.
* `Int.greatestOfBdd`: a similar definition with all inequalities reversed.

## Main statements

* `Int.exists_least_of_bdd`: if `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is
  bounded below and nonempty, then this set has the least element. This lemma uses classical logic
  to avoid assumption `[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart.

* `Int.coe_leastOfBdd_eq`: `(Int.leastOfBdd b Hb Hinh : ℤ)` does not depend on `b`.

* `Int.exists_greatest_of_bdd`, `Int.coe_greatest_of_bdd_eq`: versions of the above lemmas with all
  inequalities reversed.

## Tags

integer numbers, least element, greatest element
-/


namespace Int

/-- A computable version of `exists_least_of_bdd`: given a decidable predicate on the
integers, with an explicit lower bound and a proof that it is somewhere true, return
the least value for which the predicate is true. -/
def 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop} [
DecidablePred: {α : Sort ?u.6} → (α → Prop) → Sort (max1?u.6)
DecidablePred 
P: ℤ → Prop
P] (
b: ℤ
b : 
ℤ: Type
ℤ) (
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
b: ℤ
b ≤ 
z: ℤ
z)
    (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z) : { 
lb: ℤ
lb : 
ℤ: Type
ℤ // 
P: ℤ → Prop
P 
lb: ℤ
lb ∧ ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
lb: ℤ
lb ≤ 
z: ℤ
z } :=
  have 
EX: ∃ n, P (b + ↑n)
EX : ∃ 
n: ℕ
n : 
ℕ: Type
ℕ, 
P: ℤ → Prop
P (
b: ℤ
b + 
n: ℕ
n) :=
    let ⟨
elt: ℤ
elt, 
Helt: P elt
Helt⟩ := 
Hinh: ∃ z, P z
Hinh
    match 
elt: ℤ
elt, 
le.dest: ∀ {a b : ℤ}, a ≤ b → ∃ n, a + ↑n = b
le.dest (
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb 
_: ℤ
_ 
Helt: P elt
Helt), 
Helt: P elt
Helt with
    | _, ⟨
n: ℕ
n, 
rfl: ∀ {α : Sort ?u.226} {a : α}, a = a
rfl⟩, 
Hn: P (b + ↑n)
Hn => ⟨
n: ℕ
n, 
Hn: P (b + ↑n)
Hn⟩
  ⟨
b: ℤ
b + (
Nat.find: {p : ℕ → Prop} → [inst : DecidablePred p] → (∃ n, p n) → ℕ
Nat.find 
EX: ∃ n, P (b + ↑n)
EX : 
ℤ: Type
ℤ), 
Nat.find_spec: ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n), p (Nat.find H)
Nat.find_spec 
EX: ∃ n, P (b + ↑n)
EX, fun 
z: ?m.771
z 
h: ?m.774
h =>
    match 
z: ?m.771
z, 
le.dest: ∀ {a b : ℤ}, a ≤ b → ∃ n, a + ↑n = b
le.dest (
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb 
_: ℤ
_ 
h: ?m.774
h), 
h: ?m.774
h with
    | _, ⟨
_: ℕ
_, 
rfl: ∀ {α : Sort ?u.787} {a : α}, a = a
rfl⟩, 
h: P (b + ↑w✝)
h => 
add_le_add_left: ∀ {α : Type ?u.845} [inst : Add α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
add_le_add_left (
Int.ofNat_le: ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
Int.ofNat_le.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.find_min': ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n) {m : ℕ}, p m → Nat.find H ≤ m
Nat.find_min' 
_: ∃ n, ?m.863 n
_ 
h: P (b + ↑w✝)
h) 
_: ?m.846
_⟩
#align int.least_of_bdd 
Int.leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
Int.leastOfBdd


/--
    If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded below and nonempty,
    then this set has the least element. This lemma uses classical logic to avoid assumption
    `[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart. -/
theorem 
exists_least_of_bdd: ∀ {P : ℤ → Prop} [inst : DecidablePred P],
  (∃ b, ∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
exists_least_of_bdd
    {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop}
    [
DecidablePred: {α : Sort ?u.1732} → (α → Prop) → Sort (max1?u.1732)
DecidablePred 
P: ℤ → Prop
P]
    (
Hbdd: ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hbdd : ∃ 
b: ℤ
b : 
ℤ: Type
ℤ , ∀ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z → 
b: ℤ
b ≤ 
z: ℤ
z)
    (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z) : ∃ 
lb: ℤ
lb : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
lb: ℤ
lb ∧ ∀ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z → 
lb: ℤ
lb ≤ 
z: ℤ
z := by
Goals accomplished! 🐙
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → b ≤ z

Hinh: ∃ z, P z

∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ zlet ⟨
b: ℤ
b , 
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb⟩ := 
Hbdd: ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hbdd
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
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → b ≤ z

Hinh: ∃ z, P z

∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ zlet ⟨
lb: ℤ
lb , 
H: P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
H⟩ := 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb 
Hinh: ∃ z, P z
Hinh
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
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → b ≤ z

Hinh: ∃ z, P z

∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ zexact ⟨
lb: ℤ
lb , 
H: P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
H⟩
Goals accomplished! 🐙
#align int.exists_least_of_bdd 
Int.exists_least_of_bdd: ∀ {P : ℤ → Prop} [inst : DecidablePred P],
  (∃ b, ∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
Int.exists_least_of_bdd

theorem 
coe_leastOfBdd_eq: ∀ {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)
coe_leastOfBdd_eq {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop} [
DecidablePred: {α : Sort ?u.2166} → (α → Prop) → Sort (max1?u.2166)
DecidablePred 
P: ℤ → Prop
P] {
b: ℤ
b 
b': ℤ
b' : 
ℤ: Type
ℤ} (
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
b: ℤ
b ≤ 
z: ℤ
z)
    (
Hb': ∀ (z : ℤ), P z → b' ≤ z
Hb' : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
b': ℤ
b' ≤ 
z: ℤ
z) (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z) :
    (
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb 
Hinh: ∃ z, P z
Hinh : 
ℤ: Type
ℤ) = 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd 
b': ℤ
b' 
Hb': ∀ (z : ℤ), P z → b' ≤ z
Hb' 
Hinh: ∃ z, P z
Hinh := by
Goals accomplished! 🐙
  
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)rcases 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → b ≤ z
Hb 
Hinh: ∃ z, P z
Hinh with 
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → n ≤ z
⟨
n: ℤ
n
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → n ≤ z
, 
hn: P n
hn
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → n ≤ z
, 
h2n: ∀ (z : ℤ), P z → n ≤ z
h2n
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → n ≤ z
⟩
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

mk.intro
↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } = ↑(leastOfBdd b' Hb' Hinh)
  
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)rcases 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd 
b': ℤ
b' 
Hb': ∀ (z : ℤ), P z → b' ≤ z
Hb' 
Hinh: ∃ z, P z
Hinh with 
⟨n', hn', h2n'⟩: { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
⟨
n': ℤ
n'
⟨n', hn', h2n'⟩: { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
, 
hn': P n'
hn'
⟨n', hn', h2n'⟩: { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
, 
h2n': ∀ (z : ℤ), P z → n' ≤ z
h2n'
⟨n', hn', h2n'⟩: { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
⟩
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

mk.intro.mk.intro
↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } =   ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → n' ≤ z) }
  
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)exact 
le_antisymm: ∀ {α : Type ?u.3037} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (
h2n: ∀ (z : ℤ), P z → n ≤ z
h2n 
_: ℤ
_ 
hn': P n'
hn') (
h2n': ∀ (z : ℤ), P z → n' ≤ z
h2n' 
_: ℤ
_ 
hn: P n
hn)
Goals accomplished! 🐙
#align int.coe_least_of_bdd_eq 
Int.coe_leastOfBdd_eq: ∀ {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)
Int.coe_leastOfBdd_eq

/-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
integers, with an explicit upper bound and a proof that it is somewhere true, return
the greatest value for which the predicate is true. -/
def 
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop} [
DecidablePred: {α : Sort ?u.3167} → (α → Prop) → Sort (max1?u.3167)
DecidablePred 
P: ℤ → Prop
P] (
b: ℤ
b : 
ℤ: Type
ℤ) (
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
b: ℤ
b)
    (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z) : { 
ub: ℤ
ub : 
ℤ: Type
ℤ // 
P: ℤ → Prop
P 
ub: ℤ
ub ∧ ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
ub: ℤ
ub } :=
  have 
Hbdd': ∀ (z : ℤ), P (-z) → -b ≤ z
Hbdd' : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P (-
z: ℤ
z) → -
b: ℤ
b ≤ 
z: ℤ
z := fun 
z: ?m.3253
z 
h: ?m.3256
h => 
neg_le: ∀ {α : Type ?u.3258} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
  [inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, -a ≤ b ↔ -b ≤ a
neg_le.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 (
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb 
_: ℤ
_ 
h: ?m.3256
h)
  have 
Hinh': ∃ z, P (-z)
Hinh' : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P (-
z: ℤ
z) :=
    let ⟨
elt: ℤ
elt, 
Helt: P elt
Helt⟩ := 
Hinh: ∃ z, P z
Hinh
    ⟨-
elt: ℤ
elt, by
Goals accomplished! 🐙 
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)rw [
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)
neg_neg: ∀ {G : Type ?u.4209} [inst : InvolutiveNeg G] (a : G), - -a = a
neg_neg
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]
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;
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 
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)exact 
Helt: P elt
Helt
Goals accomplished! 🐙⟩
  let ⟨
lb: ℤ
lb, 
Plb: P (-lb)
Plb, 
al: ∀ (z : ℤ), P (-z) → lb ≤ z
al⟩ := 
leastOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → b ≤ z) → (∃ z, P z) → { lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z }
leastOfBdd (-
b: ℤ
b) 
Hbdd': ∀ (z : ℤ), P (-z) → -b ≤ z
Hbdd' 
Hinh': ∃ z, P (-z)
Hinh'
  ⟨-
lb: ℤ
lb, 
Plb: P (-lb)
Plb, fun 
z: ?m.3841
z 
h: ?m.3844
h => 
le_neg: ∀ {α : Type ?u.3846} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
  [inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ -b ↔ b ≤ -a
le_neg.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| 
al: ∀ (z : ℤ), P (-z) → lb ≤ z
al 
_: ℤ
_ <| by
Goals accomplished! 🐙 
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)rwa [
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)
neg_neg: ∀ {G : Type ?u.4286} [inst : InvolutiveNeg G] (a : G), - -a = a
neg_neg
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]
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⟩
#align int.greatest_of_bdd 
Int.greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
Int.greatestOfBdd

/--
    If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded above and nonempty,
    then this set has the greatest element. This lemma uses classical logic to avoid assumption
    `[DecidablePred P]`. See `Int.greatestOfBdd` for a constructive counterpart. -/
theorem 
exists_greatest_of_bdd: ∀ {P : ℤ → Prop} [inst : DecidablePred P],
  (∃ b, ∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
exists_greatest_of_bdd
    {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop}
    [
DecidablePred: {α : Sort ?u.4600} → (α → Prop) → Sort (max1?u.4600)
DecidablePred 
P: ℤ → Prop
P]
    (
Hbdd: ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hbdd : ∃ 
b: ℤ
b : 
ℤ: Type
ℤ , ∀ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
b: ℤ
b)
    (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z) : ∃ 
ub: ℤ
ub : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
ub: ℤ
ub ∧ ∀ 
z: ℤ
z : 
ℤ: Type
ℤ , 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
ub: ℤ
ub := by
Goals accomplished! 🐙
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → z ≤ b

Hinh: ∃ z, P z

∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ublet ⟨ 
b: ℤ
b , 
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb ⟩ := 
Hbdd: ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hbdd
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
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → z ≤ b

Hinh: ∃ z, P z

∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ublet ⟨ 
lb: ℤ
lb , 
H: P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
H ⟩ := 
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb 
Hinh: ∃ z, P z
Hinh
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
  
P: ℤ → Prop

inst✝: DecidablePred P

Hbdd: ∃ b, ∀ (z : ℤ), P z → z ≤ b

Hinh: ∃ z, P z

∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ubexact ⟨ 
lb: ℤ
lb , 
H: P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
H ⟩
Goals accomplished! 🐙
#align int.exists_greatest_of_bdd 
Int.exists_greatest_of_bdd: ∀ {P : ℤ → Prop} [inst : DecidablePred P],
  (∃ b, ∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
Int.exists_greatest_of_bdd

theorem 
coe_greatestOfBdd_eq: ∀ {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)
coe_greatestOfBdd_eq {
P: ℤ → Prop
P : 
ℤ: Type
ℤ → 
Prop: Type
Prop} [
DecidablePred: {α : Sort ?u.5034} → (α → Prop) → Sort (max1?u.5034)
DecidablePred 
P: ℤ → Prop
P] {
b: ℤ
b 
b': ℤ
b' : 
ℤ: Type
ℤ}
    (
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
b: ℤ
b) (
Hb': ∀ (z : ℤ), P z → z ≤ b'
Hb' : ∀ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z → 
z: ℤ
z ≤ 
b': ℤ
b') (
Hinh: ∃ z, P z
Hinh : ∃ 
z: ℤ
z : 
ℤ: Type
ℤ, 
P: ℤ → Prop
P 
z: ℤ
z) :
    (
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb 
Hinh: ∃ z, P z
Hinh : 
ℤ: Type
ℤ) = 
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd 
b': ℤ
b' 
Hb': ∀ (z : ℤ), P z → z ≤ b'
Hb' 
Hinh: ∃ z, P z
Hinh := by
Goals accomplished! 🐙
  
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)rcases 
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd 
b: ℤ
b 
Hb: ∀ (z : ℤ), P z → z ≤ b
Hb 
Hinh: ∃ z, P z
Hinh with 
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → z ≤ n
⟨
n: ℤ
n
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → z ≤ n
, 
hn: P n
hn
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → z ≤ n
, 
h2n: ∀ (z : ℤ), P z → z ≤ n
h2n
⟨n, hn, h2n⟩: P n ∧ ∀ (z : ℤ), P z → z ≤ n
⟩
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

mk.intro
↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } = ↑(greatestOfBdd b' Hb' Hinh)
  
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)rcases 
greatestOfBdd: {P : ℤ → Prop} →
  [inst : DecidablePred P] → (b : ℤ) → (∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
greatestOfBdd 
b': ℤ
b' 
Hb': ∀ (z : ℤ), P z → z ≤ b'
Hb' 
Hinh: ∃ z, P z
Hinh with 
⟨n', hn', h2n'⟩: { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
⟨
n': ℤ
n'
⟨n', hn', h2n'⟩: { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
, 
hn': P n'
hn'
⟨n', hn', h2n'⟩: { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
, 
h2n': ∀ (z : ℤ), P z → z ≤ n'
h2n'
⟨n', hn', h2n'⟩: { ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub }
⟩
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'

mk.intro.mk.intro
↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } =   ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → z ≤ n') }
  
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)exact 
le_antisymm: ∀ {α : Type ?u.6007} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (
h2n': ∀ (z : ℤ), P z → z ≤ n'
h2n' 
_: ℤ
_ 
hn: P n
hn) (
h2n: ∀ (z : ℤ), P z → z ≤ n
h2n 
_: ℤ
_ 
hn': P n'
hn')
Goals accomplished! 🐙
#align int.coe_greatest_of_bdd_eq 
Int.coe_greatestOfBdd_eq: ∀ {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)
Int.coe_greatestOfBdd_eq

end Int