Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-

! 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: β€ β PropP : β€: Typeβ€ β Prop: TypeProp} [DecidablePred: {Ξ± : Sort ?u.6} β (Ξ± β Prop) β Sort (max1?u.6)DecidablePred P: β€ β PropP] (b: β€b : β€: Typeβ€) (Hb: β (z : β€), P z β b β€ zHb : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β b: β€b β€ z: β€z)
(Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z) : { lb: β€lb : β€: Typeβ€ // P: β€ β PropP lb: β€lb β§ β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β lb: β€lb β€ z: β€z } :=
have EX: β n, P (b + βn)EX : β n: βn : β: Typeβ, P: β€ β PropP (b: β€b + n: βn) :=
let β¨elt: β€elt, Helt: P eltHeltβ© := Hinh: β z, P zHinh
match elt: β€elt, le.dest: β {a b : β€}, a β€ b β β n, a + βn = ble.dest (Hb: β (z : β€), P z β b β€ zHb _: β€_ Helt: P eltHelt), Helt: P eltHelt with
| _, β¨n: βn, rfl: β {Ξ± : Sort ?u.226} {a : Ξ±}, a = arflβ©, 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.771z h: ?m.774h =>
match z: ?m.771z, le.dest: β {a b : β€}, a β€ b β β n, a + βn = ble.dest (Hb: β (z : β€), P z β b β€ zHb _: β€_ h: ?m.774h), h: ?m.774h with
| _, β¨_: β_, rfl: β {Ξ± : Sort ?u.787} {a : Ξ±}, a = arflβ©, 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 + cadd_le_add_left (Int.ofNat_le: β {m n : β}, βm β€ βn β m β€ nInt.ofNat_le.2: β {a b : Prop}, (a β b) β b β a2 <| Nat.find_min': β {p : β β Prop} [inst : DecidablePred p] (H : β n, p n) {m : β}, p m β Nat.find H β€ mNat.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 β€ zexists_least_of_bdd
{P: β€ β PropP : β€: Typeβ€ β Prop: TypeProp}
[DecidablePred: {Ξ± : Sort ?u.1732} β (Ξ± β Prop) β Sort (max1?u.1732)DecidablePred P: β€ β PropP]
(Hbdd: β b, β (z : β€), P z β b β€ zHbdd : β b: β€b : β€: Typeβ€ , β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z β b: β€b β€ z: β€z)
(Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z) : β lb: β€lb : β€: Typeβ€ , P: β€ β PropP lb: β€lb β§ β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z β lb: β€lb β€ z: β€z := byGoals accomplished! π
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β b β€ zHinh: β z, P zβ lb, P lb β§ β (z : β€), P z β lb β€ zlet β¨b: β€b , Hb: β (z : β€), P z β b β€ zHbβ© := Hbdd: β b, β (z : β€), P z β b β€ zHbddP: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β b β€ zHinh: β z, P zb: β€Hb: β (z : β€), P z β b β€ zβ lb, P lb β§ β (z : β€), P z β lb β€ z
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β b β€ zHinh: β z, P zβ lb, P lb β§ β (z : β€), P z β lb β€ zlet β¨lb: β€lb , H: P lb β§ β (z : β€), P z β lb β€ zHβ© := 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 β€ zHb Hinh: β z, P zHinhP: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β b β€ zHinh: β z, P zb: β€Hb: β (z : β€), P z β b β€ zlb: β€H: P lb β§ β (z : β€), P z β lb β€ zβ lb, P lb β§ β (z : β€), P z β lb β€ z
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β b β€ zHinh: β z, P zβ lb, P lb β§ β (z : β€), P z β lb β€ zexact β¨lb: β€lb , H: P lb β§ β (z : β€), P z β lb β€ zHβ©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 β€ zInt.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: β€ β PropP : β€: Typeβ€ β Prop: TypeProp} [DecidablePred: {Ξ± : Sort ?u.2166} β (Ξ± β Prop) β Sort (max1?u.2166)DecidablePred P: β€ β PropP] {b: β€b b': β€b' : β€: Typeβ€} (Hb: β (z : β€), P z β b β€ zHb : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β b: β€b β€ z: β€z)
(Hb': β (z : β€), P z β b' β€ zHb' : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β b': β€b' β€ z: β€z) (Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€, P: β€ β PropP 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 β€ zHb Hinh: β z, P zHinh : β€: 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' β€ zHb' Hinh: β z, P zHinh := byGoals accomplished! π
P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β b β€ zHb': β (z : β€), P z β b' β€ zHinh: β 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 β€ zHb Hinh: β z, P zHinh 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 nhnβ¨n, hn, h2nβ©: P n β§ β (z : β€), P z β n β€ z, h2n: β (z : β€), P z β n β€ zh2nβ¨n, hn, h2nβ©: P n β§ β (z : β€), P z β n β€ zβ©P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β b β€ zHb': β (z : β€), P z β b' β€ zHinh: β z, P zn: β€hn: P nh2n: β (z : β€), P z β n β€ zmk.introβ{ val := n, property := (_ : P n β§ β (z : β€), P z β n β€ z) } = β(leastOfBdd b' Hb' Hinh)
P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β b β€ zHb': β (z : β€), P z β b' β€ zHinh: β 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' β€ zHb' Hinh: β z, P zHinh 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' β€ zh2n'β¨n', hn', h2n'β©: { lb // P lb β§ β (z : β€), P z β lb β€ z }β©P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β b β€ zHb': β (z : β€), P z β b' β€ zHinh: β z, P zn: β€hn: P nh2n: β (z : β€), P z β n β€ zn': β€hn': P n'h2n': β (z : β€), P z β n' β€ zmk.intro.mk.introβ{ val := n, property := (_ : P n β§ β (z : β€), P z β n β€ z) } =   β{ val := n', property := (_ : P n' β§ β (z : β€), P z β n' β€ z) }
P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β b β€ zHb': β (z : β€), P z β b' β€ zHinh: β 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 = ble_antisymm (h2n: β (z : β€), P z β n β€ zh2n _: β€_ hn': P n'hn') (h2n': β (z : β€), P z β n' β€ zh2n' _: β€_ hn: P nhn)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: β€ β PropP : β€: Typeβ€ β Prop: TypeProp} [DecidablePred: {Ξ± : Sort ?u.3167} β (Ξ± β Prop) β Sort (max1?u.3167)DecidablePred P: β€ β PropP] (b: β€b : β€: Typeβ€) (Hb: β (z : β€), P z β z β€ bHb : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β z: β€z β€ b: β€b)
(Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z) : { ub: β€ub : β€: Typeβ€ // P: β€ β PropP ub: β€ub β§ β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β z: β€z β€ ub: β€ub } :=
have Hbdd': β (z : β€), P (-z) β -b β€ zHbdd' : β z: β€z : β€: Typeβ€, P: β€ β PropP (-z: β€z) β -b: β€b β€ z: β€z := fun z: ?m.3253z h: ?m.3256h => 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 β€ aneg_le.1: β {a b : Prop}, (a β b) β a β b1 (Hb: β (z : β€), P z β z β€ bHb _: β€_ h: ?m.3256h)
have Hinh': β z, P (-z)Hinh' : β z: β€z : β€: Typeβ€, P: β€ β PropP (-z: β€z) :=
let β¨elt: β€elt, Helt: P eltHeltβ© := Hinh: β z, P zHinh
β¨-elt: β€elt, byGoals accomplished! π P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP (- -elt)rw [P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP (- -elt)neg_neg: β {G : Type ?u.4209} [inst : InvolutiveNeg G] (a : G), - -a = aneg_negP: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP elt]P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP elt;P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP elt P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zelt: β€Helt: P eltP (- -elt)exact Helt: P eltHeltGoals accomplished! πβ©
let β¨lb: β€lb, Plb: P (-lb)Plb, al: β (z : β€), P (-z) β lb β€ zalβ© := 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 β€ zHbdd' Hinh': β z, P (-z)Hinh'
β¨-lb: β€lb, Plb: P (-lb)Plb, fun z: ?m.3841z h: ?m.3844h => 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 β€ -ale_neg.1: β {a b : Prop}, (a β b) β a β b1 <| al: β (z : β€), P (-z) β lb β€ zal _: β€_ <| byGoals accomplished! π P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zHinh': β z, P (-z)lb: β€Plb: P (-lb)al: β (z : β€), P (-z) β lb β€ zz: β€h: P zP (- -z)rwa [P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zHinh': β z, P (-z)lb: β€Plb: P (-lb)al: β (z : β€), P (-z) β lb β€ zz: β€h: P zP (- -z)neg_neg: β {G : Type ?u.4286} [inst : InvolutiveNeg G] (a : G), - -a = aneg_negP: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zHinh': β z, P (-z)lb: β€Plb: P (-lb)al: β (z : β€), P (-z) β lb β€ zz: β€h: P zP z]P: β€ β Propinstβ: DecidablePred Pb: β€Hb: β (z : β€), P z β z β€ bHinh: β z, P zHbdd': β (z : β€), P (-z) β -b β€ zHinh': β z, P (-z)lb: β€Plb: P (-lb)al: β (z : β€), P (-z) β lb β€ zz: β€h: P zP 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 β€ ubexists_greatest_of_bdd
{P: β€ β PropP : β€: Typeβ€ β Prop: TypeProp}
[DecidablePred: {Ξ± : Sort ?u.4600} β (Ξ± β Prop) β Sort (max1?u.4600)DecidablePred P: β€ β PropP]
(Hbdd: β b, β (z : β€), P z β z β€ bHbdd : β b: β€b : β€: Typeβ€ , β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z β z: β€z β€ b: β€b)
(Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z) : β ub: β€ub : β€: Typeβ€ , P: β€ β PropP ub: β€ub β§ β z: β€z : β€: Typeβ€ , P: β€ β PropP z: β€z β z: β€z β€ ub: β€ub := byGoals accomplished! π
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β z β€ bHinh: β z, P zβ ub, P ub β§ β (z : β€), P z β z β€ ublet β¨ b: β€b , Hb: β (z : β€), P z β z β€ bHb β© := Hbdd: β b, β (z : β€), P z β z β€ bHbddP: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β z β€ bHinh: β z, P zb: β€Hb: β (z : β€), P z β z β€ bβ ub, P ub β§ β (z : β€), P z β z β€ ub
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β z β€ bHinh: β z, P zβ ub, P ub β§ β (z : β€), P z β z β€ ublet β¨ lb: β€lb , H: P lb β§ β (z : β€), P z β z β€ lbH β© := 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 β€ bHb Hinh: β z, P zHinhP: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β z β€ bHinh: β z, P zb: β€Hb: β (z : β€), P z β z β€ blb: β€H: P lb β§ β (z : β€), P z β z β€ lbβ ub, P ub β§ β (z : β€), P z β z β€ ub
P: β€ β Propinstβ: DecidablePred PHbdd: β b, β (z : β€), P z β z β€ bHinh: β z, P zβ ub, P ub β§ β (z : β€), P z β z β€ ubexact β¨ lb: β€lb , H: P lb β§ β (z : β€), P z β z β€ lbH β©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 β€ ubInt.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: β€ β PropP : β€: Typeβ€ β Prop: TypeProp} [DecidablePred: {Ξ± : Sort ?u.5034} β (Ξ± β Prop) β Sort (max1?u.5034)DecidablePred P: β€ β PropP] {b: β€b b': β€b' : β€: Typeβ€}
(Hb: β (z : β€), P z β z β€ bHb : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β z: β€z β€ b: β€b) (Hb': β (z : β€), P z β z β€ b'Hb' : β z: β€z : β€: Typeβ€, P: β€ β PropP z: β€z β z: β€z β€ b': β€b') (Hinh: β z, P zHinh : β z: β€z : β€: Typeβ€, P: β€ β PropP 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 β€ bHb Hinh: β z, P zHinh : β€: 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 zHinh := byGoals accomplished! π
P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β z β€ bHb': β (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 β€ bHb Hinh: β z, P zHinh 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 nhnβ¨n, hn, h2nβ©: P n β§ β (z : β€), P z β z β€ n, h2n: β (z : β€), P z β z β€ nh2nβ¨n, hn, h2nβ©: P n β§ β (z : β€), P z β z β€ nβ©P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β z β€ bHb': β (z : β€), P z β z β€ b'Hinh: β z, P zn: β€hn: P nh2n: β (z : β€), P z β z β€ nmk.introβ{ val := n, property := (_ : P n β§ β (z : β€), P z β z β€ n) } = β(greatestOfBdd b' Hb' Hinh)
P: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β z β€ bHb': β (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 zHinh 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: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β z β€ bHb': β (z : β€), P z β z β€ b'Hinh: β z, P zn: β€hn: P nh2n: β (z : β€), P z β z β€ nn': β€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: β€ β Propinstβ: DecidablePred Pb, b': β€Hb: β (z : β€), P z β z β€ bHb': β (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 = ble_antisymm (h2n': β (z : β€), P z β z β€ n'h2n' _: β€_ hn: P nhn) (h2n: β (z : β€), P z β z β€ nh2n _: β€_ 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
```