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.
```/-
Authors: Johannes HΓΆlzl

! This file was ported from Lean 3 source module order.zorn
! leanprover-community/mathlib commit 46a64b5b4268c594af770c44d9e502afc6a515cb
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Chain

/-!
# Zorn's lemmas

This file proves several formulations of Zorn's Lemma.

## Variants

The primary statement of Zorn's lemma is `exists_maximal_of_chains_bounded`. Then it is specialized
to particular relations:
* `(β€)` with `zorn_partialOrder`
* `(β)` with `zorn_subset`
* `(β)` with `zorn_superset`

Lemma names carry modifiers:
* `β`: Quantifies over a set, as opposed to over a type.
* `_nonempty`: Doesn't ask to prove that the empty chain is bounded and lets you give an element
that will be smaller than the maximal element found (the maximal element is no smaller than any
other element, but it can also be incomparable to some).

## How-to

This file comes across as confusing to those who haven't yet used it, so here is a detailed
walkthrough:
1. Know what relation on which type/set you're looking for. See Variants above. You can discharge
some conditions to Zorn's lemma directly using a `_nonempty` variant.
2. Write down the definition of your type/set, put a `suffices : β m, β a, m βΊ a β a βΊ m, { ... },`
(or whatever you actually need) followed by a `apply some_version_of_zorn`.
3. Fill in the details. This is where you start talking about chains.

A typical proof using Zorn could look like this (TODO: update to mathlib4)
```lean
lemma zorny_lemma : zorny_statement :=
begin
let s : Set Ξ± := {x | whatever x},
suffices : β x β s, β y β s, y β x β y = x, -- or with another operator
{ exact proof_post_zorn },
apply zorn_subset, -- or another variant
rintro c hcs hc,
obtain rfl | hcnemp := c.eq_empty_or_nonempty, -- you might need to disjunct on c empty or not
{ exact β¨edge_case_construction,
proof_that_edge_case_construction_respects_whatever,
exact β¨construction,
proof_that_construction_respects_whatever,
end
```

## Notes

Originally ported from Isabelle/HOL. The
[original file](https://isabelle.in.tum.de/dist/library/HOL/HOL/Zorn.html) was written by Jacques D.
Fleuriot, Tobias Nipkow, Christian Sternagel.
-/

open Classical Set

variable {Ξ±: Type ?u.2Ξ± Ξ²: Type ?u.2900Ξ² : Type _: Type (?u.3828+1)Type _} {r: Ξ± β Ξ± β Propr : Ξ±: Type ?u.121Ξ± β Ξ±: Type ?u.121Ξ± β Prop: TypeProp} {c: Set Ξ±c : Set: Type ?u.44 β Type ?u.44Set Ξ±: Type ?u.2Ξ±}

/-- Local notation for the relation being considered. -/
local infixl:50 " βΊ " => r

/-- **Zorn's lemma**

If every chain has an upper bound, then there exists a maximal element. -/
theorem exists_maximal_of_chains_bounded: (β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_chains_bounded (h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubh : β c: ?m.2272c, IsChain: {Ξ± : Type ?u.2276} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain r: Ξ± β Ξ± β Propr c: ?m.2272c β β ub: ?m.2289ub, β a: ?m.2292a β c: ?m.2272c, a: ?m.2292a βΊ ub: ?m.2289ub)
(trans: β {a b c : Ξ±}, r a b β r b c β r a ctrans : β {a: ?m.2337a b: ?m.2340b c: ?m.2343c}, a: ?m.2337a βΊ b: ?m.2340b β b: ?m.2340b βΊ c: ?m.2343c β a: ?m.2337a βΊ c: ?m.2343c) : β m: ?m.2355m, β a: ?m.2358a, m: ?m.2355m βΊ a: ?m.2358a β a: ?m.2358a βΊ m: ?m.2355m :=
have : β ub: ?m.2376ub, β a: ?m.2379a β maxChain: {Ξ± : Type ?u.2400} β (Ξ± β Ξ± β Prop) β Set Ξ±maxChain r: Ξ± β Ξ± β Propr, a: ?m.2379a βΊ ub: ?m.2376ub := h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubh _: Set Ξ±_ <| maxChain_spec: β {Ξ± : Type ?u.2443} {r : Ξ± β Ξ± β Prop}, IsMaxChain r (maxChain r)maxChain_spec.left: β {a b : Prop}, a β§ b β aleft
let β¨ub: Ξ±ub, (hub: β (a : Ξ±), a β maxChain r β r a ubhub : β a β maxChain r, a βΊ ub)β© := this: β ub, β (a : Ξ±), a β maxChain r β r a ubthis
β¨ub: Ξ±ub, fun a: ?m.2589a ha: ?m.2592ha =>
have : IsChain: {Ξ± : Type ?u.2595} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain r: Ξ± β Ξ± β Propr (insert: {Ξ± : outParam (Type ?u.2604)} β {Ξ³ : Type ?u.2603} β [self : Insert Ξ± Ξ³] β Ξ± β Ξ³ β Ξ³insert a: ?m.2589a <| maxChain: {Ξ± : Type ?u.2615} β (Ξ± β Ξ± β Prop) β Set Ξ±maxChain r: Ξ± β Ξ± β Propr) :=
maxChain_spec: β {Ξ± : Type ?u.2634} {r : Ξ± β Ξ± β Prop}, IsMaxChain r (maxChain r)maxChain_spec.1: β {a b : Prop}, a β§ b β a1.insert: β {Ξ± : Type ?u.2642} {r : Ξ± β Ξ± β Prop} {s : Set Ξ±} {a : Ξ±},
IsChain r s β (β (b : Ξ±), b β s β a β  b β r a b β¨ r b a) β IsChain r (insert a s)insert fun b: ?m.2679b hb: ?m.2682hb _: ?m.2685_ => Or.inr: β {a b : Prop}, b β a β¨ bOr.inr <| trans: β {a b c : Ξ±}, r a b β r b c β r a ctrans (hub: β (a : Ξ±), a β maxChain r β r a ubhub b: ?m.2679b hb: ?m.2682hb) ha: ?m.2592ha
hub: β (a : Ξ±), a β maxChain r β r a ubhub a: ?m.2589a <| byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.2259r: Ξ± β Ξ± β Propc: Set Ξ±h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubtrans: β {a b c : Ξ±}, r a b β r b c β r a cthisβ: β ub, β (a : Ξ±), a β maxChain r β r a ubub: Ξ±hub: β (a : Ξ±), a β maxChain r β r a uba: Ξ±ha: r ub athis: IsChain r (insert a (maxChain r))a β maxChain rrw [Ξ±: Type u_1Ξ²: Type ?u.2259r: Ξ± β Ξ± β Propc: Set Ξ±h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubtrans: β {a b c : Ξ±}, r a b β r b c β r a cthisβ: β ub, β (a : Ξ±), a β maxChain r β r a ubub: Ξ±hub: β (a : Ξ±), a β maxChain r β r a uba: Ξ±ha: r ub athis: IsChain r (insert a (maxChain r))a β maxChain rmaxChain_spec: β {Ξ± : Type ?u.2800} {r : Ξ± β Ξ± β Prop}, IsMaxChain r (maxChain r)maxChain_spec.right: β {a b : Prop}, a β§ b β bright this: IsChain r (insert a (maxChain r))this (subset_insert: β {Ξ± : Type ?u.2826} (x : Ξ±) (s : Set Ξ±), s β insert x ssubset_insert _: ?m.2827_ _: Set ?m.2827_)Ξ±: Type u_1Ξ²: Type ?u.2259r: Ξ± β Ξ± β Propc: Set Ξ±h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubtrans: β {a b c : Ξ±}, r a b β r b c β r a cthisβ: β ub, β (a : Ξ±), a β maxChain r β r a ubub: Ξ±hub: β (a : Ξ±), a β maxChain r β r a uba: Ξ±ha: r ub athis: IsChain r (insert a (maxChain r))a β insert a (maxChain r)]Ξ±: Type u_1Ξ²: Type ?u.2259r: Ξ± β Ξ± β Propc: Set Ξ±h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubtrans: β {a b c : Ξ±}, r a b β r b c β r a cthisβ: β ub, β (a : Ξ±), a β maxChain r β r a ubub: Ξ±hub: β (a : Ξ±), a β maxChain r β r a uba: Ξ±ha: r ub athis: IsChain r (insert a (maxChain r))a β insert a (maxChain r)
Ξ±: Type u_1Ξ²: Type ?u.2259r: Ξ± β Ξ± β Propc: Set Ξ±h: β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ubtrans: β {a b c : Ξ±}, r a b β r b c β r a cthisβ: β ub, β (a : Ξ±), a β maxChain r β r a ubub: Ξ±hub: β (a : Ξ±), a β maxChain r β r a uba: Ξ±ha: r ub athis: IsChain r (insert a (maxChain r))a β maxChain rexact mem_insert: β {Ξ± : Type ?u.2848} (x : Ξ±) (s : Set Ξ±), x β insert x smem_insert _: ?m.2849_ _: Set ?m.2849_Goals accomplished! πβ©
#align exists_maximal_of_chains_bounded exists_maximal_of_chains_bounded: β {Ξ± : Type u_1} {r : Ξ± β Ξ± β Prop},
(β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_chains_bounded

/-- A variant of Zorn's lemma. If every nonempty chain of a nonempty type has an upper bound, then
there is a maximal element.
-/
theorem exists_maximal_of_nonempty_chains_bounded: β [inst : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain r c β Set.Nonempty c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_nonempty_chains_bounded [Nonempty: Sort ?u.2912 β PropNonempty Ξ±: Type ?u.2897Ξ±]
(h: β (c : Set Ξ±), IsChain r c β Set.Nonempty c β β ub, β (a : Ξ±), a β c β r a ubh : β c: ?m.2916c, IsChain: {Ξ± : Type ?u.2920} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain r: Ξ± β Ξ± β Propr c: ?m.2916c β c: ?m.2916c.Nonempty: {Ξ± : Type ?u.2931} β Set Ξ± β PropNonempty β β ub: ?m.2939ub, β a: ?m.2942a β c: ?m.2916c, a: ?m.2942a βΊ ub: ?m.2939ub)
(trans: β {a b c : Ξ±}, r a b β r b c β r a ctrans : β {a: ?m.2987a b: ?m.2990b c: ?m.2993c}, a: ?m.2987a βΊ b: ?m.2990b β b: ?m.2990b βΊ c: ?m.2993c β a: ?m.2987a βΊ c: ?m.2993c) : β m: ?m.3005m, β a: ?m.3008a, m: ?m.3005m βΊ a: ?m.3008a β a: ?m.3008a βΊ m: ?m.3005m :=
exists_maximal_of_chains_bounded: β {Ξ± : Type ?u.3023} {r : Ξ± β Ξ± β Prop},
(β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_chains_bounded
(fun c: ?m.3037c hc: ?m.3040hc =>
(eq_empty_or_nonempty: β {Ξ± : Type ?u.3042} (s : Set Ξ±), s = β β¨ Set.Nonempty seq_empty_or_nonempty c: ?m.3037c).elim: β {a b c : Prop}, a β¨ b β (a β c) β (b β c) β celim
(fun h: ?m.3059h => β¨Classical.arbitrary: (Ξ± : Sort ?u.3072) β [h : Nonempty Ξ±] β Ξ±Classical.arbitrary Ξ±: Type ?u.2897Ξ±, fun x: ?m.3087x hx: ?m.3090hx => (h: ?m.3059h βΈ hx: ?m.3090hx : x: ?m.3087x β (β: ?m.3113β : Set: Type ?u.3111 β Type ?u.3111Set Ξ±: Type ?u.2897Ξ±)).elim: β {C : Sort ?u.3171}, False β Celimβ©) (h: β (c : Set Ξ±), IsChain r c β Set.Nonempty c β β ub, β (a : Ξ±), a β c β r a ubh c: ?m.3037c hc: ?m.3040hc))
trans: β {a b c : Ξ±}, r a b β r b c β r a ctrans
#align exists_maximal_of_nonempty_chains_bounded exists_maximal_of_nonempty_chains_bounded: β {Ξ± : Type u_1} {r : Ξ± β Ξ± β Prop} [inst : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain r c β Set.Nonempty c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_nonempty_chains_bounded

section Preorder

variable [Preorder: Type ?u.3266 β Type ?u.3266Preorder Ξ±: Type ?u.3251Ξ±]

theorem zorn_preorder: (β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_preorder (h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove ch : β c: Set Ξ±c : Set: Type ?u.3288 β Type ?u.3288Set Ξ±: Type ?u.3269Ξ±, IsChain: {Ξ± : Type ?u.3292} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: Set Ξ±c β BddAbove: {Ξ± : Type ?u.3353} β [inst : Preorder Ξ±] β Set Ξ± β PropBddAbove c: Set Ξ±c) :
β m: Ξ±m : Ξ±: Type ?u.3269Ξ±, β a: ?m.3385a, m: Ξ±m β€ a: ?m.3385a β a: ?m.3385a β€ m: Ξ±m :=
exists_maximal_of_chains_bounded: β {Ξ± : Type ?u.3420} {r : Ξ± β Ξ± β Prop},
(β (c : Set Ξ±), IsChain r c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_chains_bounded h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove ch le_trans: β {Ξ± : Type ?u.3454} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ cle_trans
#align zorn_preorder zorn_preorder: β {Ξ± : Type u_1} [inst : Preorder Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_preorder

theorem zorn_nonempty_preorder: β {Ξ± : Type u_1} [inst : Preorder Ξ±] [inst_1 : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_nonempty_preorder [Nonempty: Sort ?u.3528 β PropNonempty Ξ±: Type ?u.3510Ξ±]
(h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove ch : β c: Set Ξ±c : Set: Type ?u.3532 β Type ?u.3532Set Ξ±: Type ?u.3510Ξ±, IsChain: {Ξ± : Type ?u.3536} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: Set Ξ±c β c: Set Ξ±c.Nonempty: {Ξ± : Type ?u.3598} β Set Ξ± β PropNonempty β BddAbove: {Ξ± : Type ?u.3603} β [inst : Preorder Ξ±] β Set Ξ± β PropBddAbove c: Set Ξ±c) : β m: Ξ±m : Ξ±: Type ?u.3510Ξ±, β a: ?m.3636a, m: Ξ±m β€ a: ?m.3636a β a: ?m.3636a β€ m: Ξ±m :=
exists_maximal_of_nonempty_chains_bounded: β {Ξ± : Type ?u.3673} {r : Ξ± β Ξ± β Prop} [inst : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain r c β Set.Nonempty c β β ub, β (a : Ξ±), a β c β r a ub) β
(β {a b c : Ξ±}, r a b β r b c β r a c) β β m, β (a : Ξ±), r m a β r a mexists_maximal_of_nonempty_chains_bounded h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove ch le_trans: β {Ξ± : Type ?u.3754} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ cle_trans
#align zorn_nonempty_preorder zorn_nonempty_preorder: β {Ξ± : Type u_1} [inst : Preorder Ξ±] [inst_1 : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_nonempty_preorder

theorem zorn_preorderβ: β (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_preorderβ (s: Set Ξ±s : Set: Type ?u.3843 β Type ?u.3843Set Ξ±: Type ?u.3825Ξ±)
(ih: β (c : Set Ξ±) (x : c β s), IsChain (fun x_1 x_2 => x_1 β€ x_2) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih : β (c: ?m.3847c) (_: c β s_ : c: ?m.3847c β s: Set Ξ±s), IsChain: {Ξ± : Type ?u.3869} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: ?m.3847c β β ub: ?m.3932ub β s: Set Ξ±s, β z: ?m.3953z β c: ?m.3847c, z: ?m.3953z β€ ub: ?m.3932ub) :
β m: ?m.4009m β s: Set Ξ±s, β z: ?m.4028z β s: Set Ξ±s, m: ?m.4009m β€ z: ?m.4028z β z: ?m.4028z β€ m: ?m.4009m :=
let β¨β¨m: Ξ±m, hms: m β shmsβ©, h: β (a : βs), { val := m, property := hms } β€ a β a β€ { val := m, property := hms }hβ© :=
@zorn_preorder: β {Ξ± : Type ?u.4085} [inst : Preorder Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_preorder s: Set Ξ±s _ fun c: ?m.4217c hc: ?m.4220hc =>
let β¨ub: Ξ±ub, hubs: ub β shubs, hub: β (z : Ξ±), z β Subtype.val '' c β z β€ ubhubβ© :=
ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih (Subtype.val: {Ξ± : Sort ?u.4228} β {p : Ξ± β Prop} β Subtype p β Ξ±Subtype.val '' c: ?m.4217c) (fun _: ?m.4242_ β¨β¨_: Ξ±_, hx: valβ β shxβ©, _, h: β{ val := valβ, property := hx } = xβΒΉhβ© => h: β{ val := valβ, property := hx } = xβΒΉh βΈ hx: valβ β shx)
(byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.3828r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubc: Set βshc: IsChain (fun x x_1 => x β€ x_1) cIsChain (fun x x_1 => x β€ x_1) (Subtype.val '' c)rintro _: Ξ±_ β¨p, hpc, rflβ©: xβ β Subtype.val '' cβ¨p: { x // x β s }pβ¨p, hpc, rflβ©: xβ β Subtype.val '' c, hpc: p β chpcβ¨p, hpc, rflβ©: xβ β Subtype.val '' c, rfl: βp = xβrflβ¨p, hpc, rflβ©: xβ β Subtype.val '' cβ© _: Ξ±_ β¨q, hqc, rflβ©: q β c β§ βq = yββ¨q: { x // x β s }qβ¨q, hqc, rflβ©: q β c β§ βq = yβ, hqc: q β chqcβ¨q, hqc, rflβ©: q β c β§ βq = yβ, rfl: βq = yβrflβ¨q, hqc, rflβ©: q β c β§ βq = yββ© hpq: βp β  βqhpqΞ±: Type u_1Ξ²: Type ?u.3828r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubc: Set βshc: IsChain (fun x x_1 => x β€ x_1) cp: { x // x β s }hpc: p β cq: { x // x β s }hqc: q β chpq: βp β  βqintro.intro.intro.intro(fun x x_1 => x β€ x_1) βp βq β¨ (fun x x_1 => x β€ x_1) βq βp
Ξ±: Type u_1Ξ²: Type ?u.3828r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubc: Set βshc: IsChain (fun x x_1 => x β€ x_1) cIsChain (fun x x_1 => x β€ x_1) (Subtype.val '' c)refine' hc: IsChain (fun x x_1 => x β€ x_1) chc hpc: p β chpc hqc: q β chqc fun t: ?m.5408t => hpq: βp β  βqhpq (Subtype.ext_iff: β {Ξ± : Sort ?u.5410} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2Subtype.ext_iff.1: β {a b : Prop}, (a β b) β a β b1 t: ?m.5408t)Goals accomplished! π)
β¨β¨ub: Ξ±ub, hubs: ub β shubsβ©, fun β¨y: Ξ±y, hy: y β shyβ© hc: ?m.4590hc => hub: β (z : Ξ±), z β Subtype.val '' c β z β€ ubhub _: Ξ±_ β¨_: ?m.4660_, hc: { val := y, property := hy } β chc, rfl: β {Ξ± : Sort ?u.4682} {a : Ξ±}, a = arflβ©β©
β¨m: Ξ±m, hms: m β shms, fun z: ?m.5062z hzs: ?m.5065hzs hmz: ?m.5068hmz => h: β (a : βs), { val := m, property := hms } β€ a β a β€ { val := m, property := hms }h β¨z: ?m.5062z, hzs: ?m.5065hzsβ© hmz: ?m.5068hmzβ©
#align zorn_preorderβ zorn_preorderβ: β {Ξ± : Type u_1} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_preorderβ

theorem zorn_nonempty_preorderβ: β (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_nonempty_preorderβ (s: Set Ξ±s : Set: Type ?u.5549 β Type ?u.5549Set Ξ±: Type ?u.5531Ξ±)
(ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih : β (c: ?m.5553c) (_: c β s_ : c: ?m.5553c β s: Set Ξ±s), IsChain: {Ξ± : Type ?u.5575} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: ?m.5553c β β y: ?m.5636y β c: ?m.5553c, β ub: ?m.5674ub β s: Set Ξ±s, β z: ?m.5693z β c: ?m.5553c, z: ?m.5693z β€ ub: ?m.5674ub) (x: Ξ±x : Ξ±: Type ?u.5531Ξ±)
(hxs: x β shxs : x: Ξ±x β s: Set Ξ±s) : β m: ?m.5779m β s: Set Ξ±s, x: Ξ±x β€ m: ?m.5779m β§ β z: ?m.5801z β s: Set Ξ±s, m: ?m.5779m β€ z: ?m.5801z β z: ?m.5801z β€ m: ?m.5779m := byGoals accomplished! π
-- Porting note: the first three lines replace the following two lines in mathlib3.
-- The mathlib3 `rcases` supports holes for proof obligations, this is not yet implemented in 4.
-- rcases zorn_preorderβ ({ y β s | x β€ y }) fun c hcs hc => ?_ with β¨m, β¨hms, hxmβ©, hmβ©
-- Β· exact β¨m, hms, hxm, fun z hzs hmz => hm _ β¨hzs, hxm.trans hmzβ© hmzβ©
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sβ m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mhave H: ?m.5863H := zorn_preorderβ: β {Ξ± : Type ?u.5864} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_preorderβ ({ y: ?m.5872y β s: Set Ξ±s | x: Ξ±x β€ y: ?m.5872y }) fun c: ?m.5912c hcs: ?m.5915hcs hc: ?m.5918hc => ?_: β ub, ub β { y | y β s β§ x β€ y } β§ β (z : ?m.5865), z β c β z β€ ub?_Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sH: β m, m β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β { y | y β s β§ x β€ y } β m β€ z β z β€ mrefine_2β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mΞ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) crefine_1β ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ub
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sH: β m, m β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β { y | y β s β§ x β€ y } β m β€ z β z β€ mrefine_2β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mexact β¨m: Ξ±m, hms: m β shms, hxm: x β€ mhxm, fun z: ?m.6042z hzs: ?m.6045hzs hmz: ?m.6048hmz => hm: β (z : Ξ±), z β { y | y β s β§ x β€ y } β m β€ z β z β€ mhm _: Ξ±_ β¨hzs: ?m.6045hzs, hxm: x β€ mhxm.trans: β {Ξ± : Type ?u.6061} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans hmz: ?m.6048hmzβ© hmz: ?m.6048hmzβ©Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sβ m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mΒ·Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) crefine_1β ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ub Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) crefine_1β ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubrcases c: ?m.5912c.eq_empty_or_nonempty: β {Ξ± : Type ?u.6077} (s : Set Ξ±), s = β β¨ Set.Nonempty seq_empty_or_nonempty with (rfl | β¨y, hyβ©): c = β β¨ Set.Nonempty c(rfl: c = βrflrfl | β¨y, hyβ©: c = β β¨ Set.Nonempty c | β¨y, hyβ©: Set.Nonempty cβ¨y: Ξ±yβ¨y, hyβ©: Set.Nonempty c, hy: y β chyβ¨y, hyβ©: Set.Nonempty cβ©(rfl | β¨y, hyβ©): c = β β¨ Set.Nonempty c)Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β shcs: β β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) βrefine_1.inlβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β β β z β€ ubΞ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β crefine_1.inr.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ub
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) crefine_1β ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubΒ·Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β shcs: β β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) βrefine_1.inlβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β β β z β€ ub Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β shcs: β β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) βrefine_1.inlβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β β β z β€ ubΞ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β crefine_1.inr.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubexact β¨x: Ξ±x, β¨hxs: x β shxs, le_rfl: β {Ξ± : Type ?u.6179} [inst : Preorder Ξ±] {a : Ξ±}, a β€ ale_rflβ©, fun z: ?m.6197z => False.elim: β {C : Sort ?u.6199}, False β CFalse.elimβ©Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) crefine_1β ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubΒ·Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β crefine_1.inr.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ub Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β crefine_1.inr.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubrcases ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih c: ?m.5912c (fun z: ?m.6209z hz: ?m.6212hz => (hcs: ?m.5915hcs hz: ?m.6212hz).1: β {a b : Prop}, a β§ b β a1) hc: ?m.5918hc y: Ξ±y hy: y β chy with β¨z, hzs, hzβ©: β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubβ¨z: Ξ±zβ¨z, hzs, hzβ©: β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub, hzs: z β shzsβ¨z, hzs, hzβ©: β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub, hz: β (z_1 : Ξ±), z_1 β c β z_1 β€ zhzβ¨z, hzs, hzβ©: β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubβ©Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β cz: Ξ±hzs: z β shz: β (z_1 : Ξ±), z_1 β c β z_1 β€ zrefine_1.inr.intro.intro.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ub
Ξ±: Type u_1Ξ²: Type ?u.5534r: Ξ± β Ξ± β Propcβ: Set Ξ±instβ: Preorder Ξ±s: Set Ξ±ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hxs: x β sc: Set Ξ±hcs: c β { y | y β s β§ x β€ y }hc: IsChain (fun x x_1 => x β€ x_1) cy: Ξ±hy: y β crefine_1.inr.introβ ub, ub β { y | y β s β§ x β€ y } β§ β (z : Ξ±), z β c β z β€ ubexact β¨z: Ξ±z, β¨hzs: z β shzs, (hcs: ?m.5915hcs hy: y β chy).2: β {a b : Prop}, a β§ b β b2.trans: β {Ξ± : Type ?u.6304} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans <| hz: β (z_1 : Ξ±), z_1 β c β z_1 β€ zhz _: Ξ±_ hy: y β chyβ©, hz: β (z_1 : Ξ±), z_1 β c β z_1 β€ zhzβ©Goals accomplished! π
#align zorn_nonempty_preorderβ zorn_nonempty_preorderβ: β {Ξ± : Type u_1} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_nonempty_preorderβ

theorem zorn_nonempty_Iciβ: β {Ξ± : Type u_1} [inst : Preorder Ξ±] (a : Ξ±),
(β (c : Set Ξ±),
c β Ici a β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, a β€ ub β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), a β€ x β β m, x β€ m β§ β (z : Ξ±), m β€ z β z β€ mzorn_nonempty_Iciβ (a: Ξ±a : Ξ±: Type ?u.6414Ξ±)
(ih: β (c : Set Ξ±) (x : c β Ici a),
IsChain (fun x_1 x_2 => x_1 β€ x_2) c β β (y : Ξ±), y β c β β ub, a β€ ub β§ β (z : Ξ±), z β c β z β€ ubih : β (c: ?m.6435c) (_: c β Ici a_ : c: ?m.6435c β Ici: {Ξ± : Type ?u.6446} β [inst : Preorder Ξ±] β Ξ± β Set Ξ±Ici a: Ξ±a), IsChain: {Ξ± : Type ?u.6479} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: ?m.6435c β β y: ?m.6540y β c: ?m.6435c, β ub: ?m.6578ub, a: Ξ±a β€ ub: ?m.6578ub β§ β z: ?m.6592z β c: ?m.6435c, z: ?m.6592z β€ ub: ?m.6578ub)
(x: Ξ±x : Ξ±: Type ?u.6414Ξ±) (hax: a β€ xhax : a: Ξ±a β€ x: Ξ±x) : β m: ?m.6645m, x: Ξ±x β€ m: ?m.6645m β§ β z: ?m.6651z, m: ?m.6645m β€ z: ?m.6651z β z: ?m.6651z β€ m: ?m.6645m :=
let β¨m: Ξ±m, _, hxm: x β€ mhxm, hm: β (z : Ξ±), z β Ici a β m β€ z β z β€ mhmβ© := zorn_nonempty_preorderβ: β {Ξ± : Type ?u.6679} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_nonempty_preorderβ (Ici: {Ξ± : Type ?u.6682} β [inst : Preorder Ξ±] β Ξ± β Set Ξ±Ici a: Ξ±a) (byGoals accomplished! π Ξ±: Type u_1Ξ²: Type ?u.6417r: Ξ± β Ξ± β Propc: Set Ξ±instβ: Preorder Ξ±a: Ξ±ih: β (c : Set Ξ±),
c β Ici a β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, a β€ ub β§ β (z : Ξ±), z β c β z β€ ubx: Ξ±hax: a β€ xβ (c : Set Ξ±),
c β Ici a β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β Ici a β§ β (z : Ξ±), z β c β z β€ ubsimpa using ih: β (c : Set Ξ±),
c β Ici a β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, a β€ ub β§ β (z : Ξ±), z β c β z β€ ubihGoals accomplished! π) x: Ξ±x hax: a β€ xhax
β¨m: Ξ±m, hxm: x β€ mhxm, fun z: ?m.6829z hmz: ?m.6832hmz => hm: β (z : Ξ±), z β Ici a β m β€ z β z β€ mhm _: Ξ±_ (hax: a β€ xhax.trans: β {Ξ± : Type ?u.6839} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans <| hxm: x β€ mhxm.trans: β {Ξ± : Type ?u.6854} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans hmz: ?m.6832hmz) hmz: ?m.6832hmzβ©
#align zorn_nonempty_Iciβ zorn_nonempty_Iciβ: β {Ξ± : Type u_1} [inst : Preorder Ξ±] (a : Ξ±),
(β (c : Set Ξ±),
c β Ici a β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, a β€ ub β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), a β€ x β β m, x β€ m β§ β (z : Ξ±), m β€ z β z β€ mzorn_nonempty_Iciβ

end Preorder

section PartialOrder

variable [PartialOrder: Type ?u.14751 β Type ?u.14751PartialOrder Ξ±: Type ?u.14718Ξ±]

theorem zorn_partialOrder: (β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a = mzorn_partialOrder (h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove ch : β c: Set Ξ±c : Set: Type ?u.14755 β Type ?u.14755Set Ξ±: Type ?u.14736Ξ±, IsChain: {Ξ± : Type ?u.14759} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: Set Ξ±c β BddAbove: {Ξ± : Type ?u.14820} β [inst : Preorder Ξ±] β Set Ξ± β PropBddAbove c: Set Ξ±c) :
β m: Ξ±m : Ξ±: Type ?u.14736Ξ±, β a: ?m.14866a, m: Ξ±m β€ a: ?m.14866a β a: ?m.14866a = m: Ξ±m :=
let β¨m: Ξ±m, hm: β (a : Ξ±), m β€ a β a β€ mhmβ© := zorn_preorder: β {Ξ± : Type ?u.14908} [inst : Preorder Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_preorder h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove ch
β¨m: Ξ±m, fun a: ?m.15018a ha: ?m.15021ha => le_antisymm: β {Ξ± : Type ?u.15023} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm (hm: β (a : Ξ±), m β€ a β a β€ mhm a: ?m.15018a ha: ?m.15021ha) ha: ?m.15021haβ©
#align zorn_partial_order zorn_partialOrder: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a = mzorn_partialOrder

theorem zorn_nonempty_partialOrder: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±] [inst_1 : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a = mzorn_nonempty_partialOrder [Nonempty: Sort ?u.15208 β PropNonempty Ξ±: Type ?u.15190Ξ±]
(h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove ch : β c: Set Ξ±c : Set: Type ?u.15212 β Type ?u.15212Set Ξ±: Type ?u.15190Ξ±, IsChain: {Ξ± : Type ?u.15216} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: Set Ξ±c β c: Set Ξ±c.Nonempty: {Ξ± : Type ?u.15278} β Set Ξ± β PropNonempty β BddAbove: {Ξ± : Type ?u.15283} β [inst : Preorder Ξ±] β Set Ξ± β PropBddAbove c: Set Ξ±c) : β m: Ξ±m : Ξ±: Type ?u.15190Ξ±, β a: ?m.15330a, m: Ξ±m β€ a: ?m.15330a β a: ?m.15330a = m: Ξ±m :=
let β¨m: Ξ±m, hm: β (a : Ξ±), m β€ a β a β€ mhmβ© := zorn_nonempty_preorder: β {Ξ± : Type ?u.15374} [inst : Preorder Ξ±] [inst_1 : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a β€ mzorn_nonempty_preorder h: β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove ch
β¨m: Ξ±m, fun a: ?m.15503a ha: ?m.15506ha => le_antisymm: β {Ξ± : Type ?u.15508} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm (hm: β (a : Ξ±), m β€ a β a β€ mhm a: ?m.15503a ha: ?m.15506ha) ha: ?m.15506haβ©
#align zorn_nonempty_partial_order zorn_nonempty_partialOrder: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±] [inst_1 : Nonempty Ξ±],
(β (c : Set Ξ±), IsChain (fun x x_1 => x β€ x_1) c β Set.Nonempty c β BddAbove c) β β m, β (a : Ξ±), m β€ a β a = mzorn_nonempty_partialOrder

theorem zorn_partialOrderβ: β (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_partialOrderβ (s: Set Ξ±s : Set: Type ?u.15684 β Type ?u.15684Set Ξ±: Type ?u.15666Ξ±)
(ih: β (c : Set Ξ±) (x : c β s), IsChain (fun x_1 x_2 => x_1 β€ x_2) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih : β (c: ?m.15688c) (_: c β s_ : c: ?m.15688c β s: Set Ξ±s), IsChain: {Ξ± : Type ?u.15710} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: ?m.15688c β β ub: ?m.15773ub β s: Set Ξ±s, β z: ?m.15794z β c: ?m.15688c, z: ?m.15794z β€ ub: ?m.15773ub) :
β m: ?m.15861m β s: Set Ξ±s, β z: ?m.15880z β s: Set Ξ±s, m: ?m.15861m β€ z: ?m.15880z β z: ?m.15880z = m: ?m.15861m :=
let β¨m: Ξ±m, hms: m β shms, hm: β (z : Ξ±), z β s β m β€ z β z β€ mhmβ© := zorn_preorderβ: β {Ξ± : Type ?u.15936} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_preorderβ s: Set Ξ±s ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih
β¨m: Ξ±m, hms: m β shms, fun z: ?m.16087z hzs: ?m.16090hzs hmz: ?m.16093hmz => (hm: β (z : Ξ±), z β s β m β€ z β z β€ mhm z: ?m.16087z hzs: ?m.16090hzs hmz: ?m.16093hmz).antisymm: β {Ξ± : Type ?u.16095} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = bantisymm hmz: ?m.16093hmzβ©
#align zorn_partial_orderβ zorn_partialOrderβ: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_partialOrderβ

theorem zorn_nonempty_partialOrderβ: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_nonempty_partialOrderβ (s: Set Ξ±s : Set: Type ?u.16343 β Type ?u.16343Set Ξ±: Type ?u.16325Ξ±)
(ih: β (c : Set Ξ±) (x : c β s),
IsChain (fun x_1 x_2 => x_1 β€ x_2) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih : β (c: ?m.16347c) (_: c β s_ : c: ?m.16347c β s: Set Ξ±s), IsChain: {Ξ± : Type ?u.16369} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β€ Β·): Ξ± β Ξ± β Prop(Β· β€ Β·) c: ?m.16347c β β y: ?m.16430y β c: ?m.16347c, β ub: ?m.16468ub β s: Set Ξ±s, β z: ?m.16487z β c: ?m.16347c, z: ?m.16487z β€ ub: ?m.16468ub) (x: Ξ±x : Ξ±: Type ?u.16325Ξ±)
(hxs: x β shxs : x: Ξ±x β s: Set Ξ±s) : β m: ?m.16584m β s: Set Ξ±s, x: Ξ±x β€ m: ?m.16584m β§ β z: ?m.16606z β s: Set Ξ±s, m: ?m.16584m β€ z: ?m.16606z β z: ?m.16606z = m: ?m.16584m :=
let β¨m: Ξ±m, hms: m β shms, hxm: x β€ mhxm, hm: β (z : Ξ±), z β s β m β€ z β z β€ mhmβ© := zorn_nonempty_preorderβ: β {Ξ± : Type ?u.16664} [inst : Preorder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z β€ mzorn_nonempty_preorderβ s: Set Ξ±s ih: β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ubih x: Ξ±x hxs: x β shxs
β¨m: Ξ±m, hms: m β shms, hxm: x β€ mhxm, fun z: ?m.16841z hzs: ?m.16844hzs hmz: ?m.16847hmz => (hm: β (z : Ξ±), z β s β m β€ z β z β€ mhm z: ?m.16841z hzs: ?m.16844hzs hmz: ?m.16847hmz).antisymm: β {Ξ± : Type ?u.16849} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = bantisymm hmz: ?m.16847hmzβ©
#align zorn_nonempty_partial_orderβ zorn_nonempty_partialOrderβ: β {Ξ± : Type u_1} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_nonempty_partialOrderβ

end PartialOrder

theorem zorn_subset: β (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ub) β
β m, m β S β§ β (a : Set Ξ±), a β S β m β a β a = mzorn_subset (S: Set (Set Ξ±)S : Set: Type ?u.17133 β Type ?u.17133Set (Set: Type ?u.17134 β Type ?u.17134Set Ξ±: Type ?u.17118Ξ±))
(h: β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ubh : β (c: ?m.17138c) (_: c β S_ : c: ?m.17138c β S: Set (Set Ξ±)S), IsChain: {Ξ± : Type ?u.17160} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β Β·): Set Ξ± β Set Ξ± β Prop(Β· β Β·) c: ?m.17138c β β ub: ?m.17189ub β S: Set (Set Ξ±)S, β s: ?m.17210s β c: ?m.17138c, s: ?m.17210s β ub: ?m.17189ub) :
β m: ?m.17266m β S: Set (Set Ξ±)S, β a: ?m.17285a β S: Set (Set Ξ±)S, m: ?m.17266m β a: ?m.17285a β a: ?m.17285a = m: ?m.17266m :=
zorn_partialOrderβ: β {Ξ± : Type ?u.17350} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_partialOrderβ S: Set (Set Ξ±)S h: β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ubh
#align zorn_subset zorn_subset: β {Ξ± : Type u_1} (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ub) β
β m, m β S β§ β (a : Set Ξ±), a β S β m β a β a = mzorn_subset

theorem zorn_subset_nonempty: β (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ub) β
β (x : Set Ξ±), x β S β β m, m β S β§ x β m β§ β (a : Set Ξ±), a β S β m β a β a = mzorn_subset_nonempty (S: Set (Set Ξ±)S : Set: Type ?u.17464 β Type ?u.17464Set (Set: Type ?u.17465 β Type ?u.17465Set Ξ±: Type ?u.17449Ξ±))
(H: β (c : Set (Set Ξ±)) (x : c β S),
IsChain (fun x_1 x_2 => x_1 β x_2) c β Set.Nonempty c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ubH : β (c: ?m.17469c) (_: c β S_ : c: ?m.17469c β S: Set (Set Ξ±)S), IsChain: {Ξ± : Type ?u.17491} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β Β·): Set Ξ± β Set Ξ± β Prop(Β· β Β·) c: ?m.17469c β c: ?m.17469c.Nonempty: {Ξ± : Type ?u.17518} β Set Ξ± β PropNonempty β β ub: ?m.17526ub β S: Set (Set Ξ±)S, β s: ?m.17547s β c: ?m.17469c, s: ?m.17547s β ub: ?m.17526ub) (x: Set Ξ±x)
(hx: x β Shx : x: ?m.17600x β S: Set (Set Ξ±)S) : β m: ?m.17636m β S: Set (Set Ξ±)S, x: ?m.17600x β m: ?m.17636m β§ β a: ?m.17660a β S: Set (Set Ξ±)S, m: ?m.17636m β a: ?m.17660a β a: ?m.17660a = m: ?m.17636m :=
zorn_nonempty_partialOrderβ: β {Ξ± : Type ?u.17727} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_nonempty_partialOrderβ _: Set ?m.17728_ (fun _: ?m.17732_ cS: ?m.17735cS hc: ?m.17738hc y: ?m.17741y yc: ?m.17744yc => H: β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ubH _: Set (Set Ξ±)_ cS: ?m.17735cS hc: ?m.17738hc β¨y: ?m.17741y, yc: ?m.17744ycβ©) _: ?m.17728_ hx: x β Shx
#align zorn_subset_nonempty zorn_subset_nonempty: β {Ξ± : Type u_1} (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ub) β
β (x : Set Ξ±), x β S β β m, m β S β§ x β m β§ β (a : Set Ξ±), a β S β m β a β a = mzorn_subset_nonempty

theorem zorn_superset: β (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β s) β
β m, m β S β§ β (a : Set Ξ±), a β S β a β m β a = mzorn_superset (S: Set (Set Ξ±)S : Set: Type ?u.17904 β Type ?u.17904Set (Set: Type ?u.17905 β Type ?u.17905Set Ξ±: Type ?u.17889Ξ±))
(h: β (c : Set (Set Ξ±)) (x : c β S), IsChain (fun x_1 x_2 => x_1 β x_2) c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β sh : β (c: ?m.17909c) (_: c β S_ : c: ?m.17909c β S: Set (Set Ξ±)S), IsChain: {Ξ± : Type ?u.17931} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β Β·): Set Ξ± β Set Ξ± β Prop(Β· β Β·) c: ?m.17909c β β lb: ?m.17960lb β S: Set (Set Ξ±)S, β s: ?m.17981s β c: ?m.17909c, lb: ?m.17960lb β s: ?m.17981s) :
β m: ?m.18037m β S: Set (Set Ξ±)S, β a: ?m.18056a β S: Set (Set Ξ±)S, a: ?m.18056a β m: ?m.18037m β a: ?m.18056a = m: ?m.18037m :=
(@zorn_partialOrderβ: β {Ξ± : Type ?u.18121} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±), c β s β IsChain (fun x x_1 => x β€ x_1) c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β m, m β s β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_partialOrderβ (Set: Type ?u.18123 β Type ?u.18123Set Ξ±: Type ?u.17889Ξ±)α΅α΅ _ S: Set (Set Ξ±)S) fun c: ?m.18194c cS: ?m.18197cS hc: ?m.18200hc => h: β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β sh c: ?m.18194c cS: ?m.18197cS hc: ?m.18200hc.symm: β {Ξ± : Type ?u.18211} {r : Ξ± β Ξ± β Prop} {s : Set Ξ±}, IsChain r s β IsChain (flip r) ssymm
#align zorn_superset zorn_superset: β {Ξ± : Type u_1} (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)), c β S β IsChain (fun x x_1 => x β x_1) c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β s) β
β m, m β S β§ β (a : Set Ξ±), a β S β a β m β a = mzorn_superset

theorem zorn_superset_nonempty: β (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β s) β
β (x : Set Ξ±), x β S β β m, m β S β§ m β x β§ β (a : Set Ξ±), a β S β a β m β a = mzorn_superset_nonempty (S: Set (Set Ξ±)S : Set: Type ?u.18293 β Type ?u.18293Set (Set: Type ?u.18294 β Type ?u.18294Set Ξ±: Type ?u.18278Ξ±))
(H: β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β sH : β (c: ?m.18298c) (_: c β S_ : c: ?m.18298c β S: Set (Set Ξ±)S), IsChain: {Ξ± : Type ?u.18320} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain (Β· β Β·): Set Ξ± β Set Ξ± β Prop(Β· β Β·) c: ?m.18298c β c: ?m.18298c.Nonempty: {Ξ± : Type ?u.18347} β Set Ξ± β PropNonempty β β lb: ?m.18355lb β S: Set (Set Ξ±)S, β s: ?m.18376s β c: ?m.18298c, lb: ?m.18355lb β s: ?m.18376s) (x: Set Ξ±x)
(hx: x β Shx : x: ?m.18429x β S: Set (Set Ξ±)S) : β m: ?m.18465m β S: Set (Set Ξ±)S, m: ?m.18465m β x: ?m.18429x β§ β a: ?m.18489a β S: Set (Set Ξ±)S, a: ?m.18489a β m: ?m.18465m β a: ?m.18489a = m: ?m.18465m :=
@zorn_nonempty_partialOrderβ: β {Ξ± : Type ?u.18556} [inst : PartialOrder Ξ±] (s : Set Ξ±),
(β (c : Set Ξ±),
c β s β IsChain (fun x x_1 => x β€ x_1) c β β (y : Ξ±), y β c β β ub, ub β s β§ β (z : Ξ±), z β c β z β€ ub) β
β (x : Ξ±), x β s β β m, m β s β§ x β€ m β§ β (z : Ξ±), z β s β m β€ z β z = mzorn_nonempty_partialOrderβ (Set: Type ?u.18558 β Type ?u.18558Set Ξ±: Type ?u.18278Ξ±)α΅α΅ _ S: Set (Set Ξ±)S (fun _: ?m.18563_ cS: ?m.18566cS hc: ?m.18569hc y: ?m.18572y yc: ?m.18575yc => H: β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β sH _: Set (Set Ξ±)_ cS: ?m.18566cS hc: ?m.18569hc.symm: β {Ξ± : Type ?u.18655} {r : Ξ± β Ξ± β Prop} {s : Set Ξ±}, IsChain r s β IsChain (flip r) ssymm β¨y: ?m.18572y, yc: ?m.18575ycβ©) _: (Set Ξ±)α΅α΅_ hx: x β Shx
#align zorn_superset_nonempty zorn_superset_nonempty: β {Ξ± : Type u_1} (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β lb, lb β S β§ β (s : Set Ξ±), s β c β lb β s) β
β (x : Set Ξ±), x β S β β m, m β S β§ m β x β§ β (a : Set Ξ±), a β S β a β m β a = mzorn_superset_nonempty

/-- Every chain is contained in a maximal chain. This generalizes Hausdorff's maximality principle.
-/
theorem IsChain.exists_maxChain: IsChain r c β β M, IsMaxChain r M β§ c β MIsChain.exists_maxChain (hc: IsChain r chc : IsChain: {Ξ± : Type ?u.18766} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain r: Ξ± β Ξ± β Propr c: Set Ξ±c) : β M: ?m.18781M, @IsMaxChain: {Ξ± : Type ?u.18783} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsMaxChain _: Type ?u.18783_ r: Ξ± β Ξ± β Propr M: ?m.18781M β§ c: Set Ξ±c β M: ?m.18781M := byGoals accomplished! π
-- Porting note: the first three lines replace the following two lines in mathlib3.
-- The mathlib3 `obtain` supports holes for proof obligations, this is not yet implemented in 4.
--   zorn_subset_nonempty { s | c β s β§ IsChain r s } _ c β¨Subset.rfl, hcβ©
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mhave H: ?m.18809H := zorn_subset_nonempty: β {Ξ± : Type ?u.18810} (S : Set (Set Ξ±)),
(β (c : Set (Set Ξ±)),
c β S β IsChain (fun x x_1 => x β x_1) c β Set.Nonempty c β β ub, ub β S β§ β (s : Set Ξ±), s β c β s β ub) β
β (x : Set Ξ±), x β S β β m, m β S β§ x β m β§ β (a : Set Ξ±), a β S β m β a β a = mzorn_subset_nonempty { s: ?m.18817s | c: Set Ξ±c β s: ?m.18817s β§ IsChain: {Ξ± : Type ?u.18831} β (Ξ± β Ξ± β Prop) β Set Ξ± β PropIsChain r: Ξ± β Ξ± β Propr s: ?m.18817s } ?_: β (c_1 : Set (Set ?m.18811)),
c_1 β { s | c β s β§ IsChain r s } β
IsChain (fun x x_1 => x β x_1) c_1 β
Set.Nonempty c_1 β β ub, ub β { s | c β s β§ IsChain r s } β§ β (s : Set ?m.18811), s β c_1 β s β ub?_ c: Set Ξ±c β¨Subset.rfl: β {Ξ± : Type ?u.18853} {s : Set Ξ±}, s β sSubset.rfl, hc: IsChain r chcβ©Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cH: β m, m β { s | c β s β§ IsChain r s } β§ c β m β§ β (a : Set Ξ±), a β { s | c β s β§ IsChain r s } β m β a β a = mrefine_2β M, IsMaxChain r M β§ c β MΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r crefine_1β (c_1 : Set (Set Ξ±)),
c_1 β { s | c β s β§ IsChain r s } β
IsChain (fun x x_1 => x β x_1) c_1 β
Set.Nonempty c_1 β β ub, ub β { s | c β s β§ IsChain r s } β§ β (s : Set Ξ±), s β c_1 β s β ub
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β MΒ·Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cH: β m, m β { s | c β s β§ IsChain r s } β§ c β m β§ β (a : Set Ξ±), a β { s | c β s β§ IsChain r s } β m β a β a = mrefine_2β M, IsMaxChain r M β§ c β M Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cH: β m, m β { s | c β s β§ IsChain r s } β§ c β m β§ β (a : Set Ξ±), a β { s | c β s β§ IsChain r s } β m β a β a = mrefine_2β M, IsMaxChain r M β§ c β MΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r crefine_1β (c_1 : Set (Set Ξ±)),
c_1 β { s | c β s β§ IsChain r s } β
IsChain (fun x x_1 => x β x_1) c_1 β
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cH: β m, m β { s | c β s β§ IsChain r s } β§ c β m β§ β (a : Set Ξ±), a β { s | c β s β§ IsChain r s } β m β a β a = mrefine_2β M, IsMaxChain r M β§ c β Mexact β¨M: Set Ξ±M, β¨hMβ: IsChain r MhMβ, fun d: ?m.18978d hd: ?m.18981hd hMd: ?m.18984hMd => (hMβ: β (a : Set Ξ±), a β { s | c β s β§ IsChain r s } β M β a β a = MhMβ _: Set Ξ±_ β¨hMβ: c β MhMβ.trans: β {Ξ± : Type ?u.18993} [inst : HasSubset Ξ±] [inst_1 : IsTrans Ξ± fun x x_1 => x β x_1] {a b c : Ξ±}, a β b β b β c β a β ctrans hMd: ?m.18984hMd, hd: ?m.18981hdβ© hMd: ?m.18984hMd).symm: β {Ξ± : Sort ?u.19033} {a b : Ξ±}, a = b β b = asymmβ©, hMβ: c β MhMββ©Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mrintro cs: Set (Set ?m.18811)cs hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ hcsβ: IsChain (fun x x_1 => x β x_1) cshcsβ β¨s, hsβ©: Set.Nonempty csβ¨s: Set Ξ±sβ¨s, hsβ©: Set.Nonempty cs, hs: s β cshsβ¨s, hsβ©: Set.Nonempty csβ©Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csrefine_1.introβ ub, ub β { s | c β s β§ IsChain r s } β§ β (s : Set Ξ±), s β cs β s β ub
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mrefine'
β¨ββcs: Set (Set ?m.18811)cs, β¨fun _: ?m.19109_ ha: ?m.19112ha => Set.mem_sUnion_of_mem: β {Ξ± : Type ?u.19114} {x : Ξ±} {t : Set Ξ±} {S : Set (Set Ξ±)}, x β t β t β S β x β ββ SSet.mem_sUnion_of_mem ((hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ hs: s β cshs).left: β {a b : Prop}, a β§ b β aleft ha: ?m.19112ha) hs: s β cshs, _: ?m.19107_β©, fun _: ?m.19136_ =>
Set.subset_sUnion_of_mem: β {Ξ± : Type ?u.19138} {S : Set (Set Ξ±)} {t : Set Ξ±}, t β S β t β ββ SSet.subset_sUnion_of_memβ©Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csrefine_1.introIsChain r (ββ cs)
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mrintro y: Ξ±y β¨sy, hsy, hysyβ©: y β ββ csβ¨sy: Set Ξ±syβ¨sy, hsy, hysyβ©: y β ββ cs, hsy: sy β cshsyβ¨sy, hsy, hysyβ©: y β ββ cs, hysy: y β syhysyβ¨sy, hsy, hysyβ©: y β ββ csβ© z: Ξ±z β¨sz, hsz, hzszβ©: sz β cs β§ z β szβ¨sz: Set Ξ±szβ¨sz, hsz, hzszβ©: sz β cs β§ z β sz, hsz: sz β cshszβ¨sz, hsz, hzszβ©: sz β cs β§ z β sz, hzsz: z β szhzszβ¨sz, hsz, hzszβ©: sz β cs β§ z β szβ© hyz: y β  zhyzΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zrefine_1.intro.intro.intro.intro.intror y z β¨ r z y
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mobtain rfl: sy = szrflrfl | hsseq: sy = sz β¨ sy β  sz | hsseq: sy β  szhsseq := eq_or_ne: β {Ξ± : Sort ?u.19244} (x y : Ξ±), x = y β¨ x β  yeq_or_ne sy: Set Ξ±sy sz: Set Ξ±szΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±hyz: y β  zhsz: sy β cshzsz: z β syrefine_1.intro.intro.intro.intro.intro.inlr y z β¨ r z yΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szrefine_1.intro.intro.intro.intro.intro.inrr y z β¨ r z y
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β MΒ·Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±hyz: y β  zhsz: sy β cshzsz: z β syrefine_1.intro.intro.intro.intro.intro.inlr y z β¨ r z y Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±hyz: y β  zhsz: sy β cshzsz: z β syrefine_1.intro.intro.intro.intro.intro.inlr y z β¨ r z yΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szrefine_1.intro.intro.intro.intro.intro.inrr y z β¨ r z yexact (hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ hsy: sy β cshsy).right: β {a b : Prop}, a β§ b β bright hysy: y β syhysy hzsz: z β syhzsz hyz: y β  zhyzGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β Mcases' hcsβ: IsChain (fun x x_1 => x β x_1) cshcsβ hsy: sy β cshsy hsz: sz β cshsz hsseq: sy β  szhsseq with h: ?m.19340h h: ?m.19341hΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sy szrefine_1.intro.intro.intro.intro.intro.inr.inlr y z β¨ r z yΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sz syrefine_1.intro.intro.intro.intro.intro.inr.inrr y z β¨ r z y
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β MΒ·Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sy szrefine_1.intro.intro.intro.intro.intro.inr.inlr y z β¨ r z y Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sy szrefine_1.intro.intro.intro.intro.intro.inr.inlr y z β¨ r z yΞ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sz syrefine_1.intro.intro.intro.intro.intro.inr.inrr y z β¨ r z yexact (hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ hsz: sz β cshsz).right: β {a b : Prop}, a β§ b β bright (h: ?m.19340h hysy: y β syhysy) hzsz: z β szhzsz hyz: y β  zhyzGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r cβ M, IsMaxChain r M β§ c β MΒ·Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sz syrefine_1.intro.intro.intro.intro.intro.inr.inrr y z β¨ r z y Ξ±: Type u_1Ξ²: Type ?u.18754r: Ξ± β Ξ± β Propc: Set Ξ±hc: IsChain r ccs: Set (Set Ξ±)hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ: IsChain (fun x x_1 => x β x_1) css: Set Ξ±hs: s β csy: Ξ±sy: Set Ξ±hsy: sy β cshysy: y β syz: Ξ±sz: Set Ξ±hsz: sz β cshzsz: z β szhyz: y β  zhsseq: sy β  szh: (fun x x_1 => x β x_1) sz syrefine_1.intro.intro.intro.intro.intro.inr.inrr y z β¨ r z yexact (hcsβ: cs β { s | c β s β§ IsChain r s }hcsβ hsy: sy β cshsy).right: β {a b : Prop}, a β§ b β bright hysy: y β syhysy (h: ?m.19341h hzsz: z β szhzsz) hyz: y β  zhyzGoals accomplished! π
#align is_chain.exists_max_chain IsChain.exists_maxChain: β {Ξ± : Type u_1} {r : Ξ± β Ξ± β Prop} {c : Set Ξ±}, IsChain r c β β M, IsMaxChain r M β§ c β MIsChain.exists_maxChain
```