/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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,
      proof_that_edge_case_construction_contains_all_stuff_in_c⟩ },
  exact ⟨construction,
    proof_that_construction_respects_whatever,
    proof_that_construction_contains_all_stuff_in_c⟩,
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: α → α → Prop
r : α: Type ?u.121
α → α: Type ?u.121
α → Prop: Type
Prop} {c: Set α
c : Set: Type ?u.44 → Type ?u.44
Set α: 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 m
exists_maximal_of_chains_bounded (h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
h : ∀ c: ?m.2272
c, IsChain: {α : Type ?u.2276} → (α → α → Prop) → Set α → Prop
IsChain r: α → α → Prop
r c: ?m.2272
c → ∃ ub: ?m.2289
ub, ∀ a: ?m.2292
a ∈ c: ?m.2272
c, a: ?m.2292
a ≺ ub: ?m.2289
ub)
    (trans: ∀ {a b c : α}, r a b → r b c → r a c
trans : ∀ {a: ?m.2337
a b: ?m.2340
b c: ?m.2343
c}, a: ?m.2337
a ≺ b: ?m.2340
b → b: ?m.2340
b ≺ c: ?m.2343
c → a: ?m.2337
a ≺ c: ?m.2343
c) : ∃ m: ?m.2355
m, ∀ a: ?m.2358
a, m: ?m.2355
m ≺ a: ?m.2358
a → a: ?m.2358
a ≺ m: ?m.2355
m :=
  have : ∃ ub: ?m.2376
ub, ∀ a: ?m.2379
a ∈ maxChain: {α : Type ?u.2400} → (α → α → Prop) → Set α
maxChain r: α → α → Prop
r, a: ?m.2379
a ≺ ub: ?m.2376
ub := h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
h _: Set α
_ <| maxChain_spec: ∀ {α : Type ?u.2443} {r : α → α → Prop}, IsMaxChain r (maxChain r)
maxChain_spec.left: ∀ {a b : Prop}, a ∧ b → a
left
  let ⟨ub: α
ub, (hub: ∀ (a : α), a ∈ maxChain r → r a ub
hub : ∀ a ∈ maxChain r, a ≺ ub)⟩ := this: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub
this
  ⟨ub: α
ub, fun a: ?m.2589
a ha: ?m.2592
ha =>
    have : IsChain: {α : Type ?u.2595} → (α → α → Prop) → Set α → Prop
IsChain r: α → α → Prop
r (insert: {α : outParam (Type ?u.2604)} → {γ : Type ?u.2603} → [self : Insert α γ] → α → γ → γ
insert a: ?m.2589
a <| maxChain: {α : Type ?u.2615} → (α → α → Prop) → Set α
maxChain r: α → α → Prop
r) :=
      maxChain_spec: ∀ {α : Type ?u.2634} {r : α → α → Prop}, IsMaxChain r (maxChain r)
maxChain_spec.1: ∀ {a b : Prop}, a ∧ b → a
1.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.2679
b hb: ?m.2682
hb _: ?m.2685
_ => Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr <| trans: ∀ {a b c : α}, r a b → r b c → r a c
trans (hub: ∀ (a : α), a ∈ maxChain r → r a ub
hub b: ?m.2679
b hb: ?m.2682
hb) ha: ?m.2592
ha
    hub: ∀ (a : α), a ∈ maxChain r → r a ub
hub a: ?m.2589
a <| by
Goals accomplished! 🐙
      α: Type u_1

β: Type ?u.2259

r: α → α → Prop

c: Set α

h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub

trans: ∀ {a b c : α}, r a b → r b c → r a c

this✝: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub

ub: α

hub: ∀ (a : α), a ∈ maxChain r → r a ub

a: α

ha: r ub a

this: IsChain r (insert a (maxChain r))

a ∈ maxChain rrw [α: Type u_1

β: Type ?u.2259

r: α → α → Prop

c: Set α

h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub

trans: ∀ {a b c : α}, r a b → r b c → r a c

this✝: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub

ub: α

hub: ∀ (a : α), a ∈ maxChain r → r a ub

a: α

ha: r ub a

this: 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 → b
right this: IsChain r (insert a (maxChain r))
this (subset_insert: ∀ {α : Type ?u.2826} (x : α) (s : Set α), s ⊆ insert x s
subset_insert _: ?m.2827
_ _: Set ?m.2827
_)α: Type u_1

β: Type ?u.2259

r: α → α → Prop

c: Set α

h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub

trans: ∀ {a b c : α}, r a b → r b c → r a c

this✝: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub

ub: α

hub: ∀ (a : α), a ∈ maxChain r → r a ub

a: α

ha: r ub a

this: IsChain r (insert a (maxChain r))

a ∈ insert a (maxChain r)]α: Type u_1

β: Type ?u.2259

r: α → α → Prop

c: Set α

h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub

trans: ∀ {a b c : α}, r a b → r b c → r a c

this✝: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub

ub: α

hub: ∀ (a : α), a ∈ maxChain r → r a ub

a: α

ha: r ub a

this: IsChain r (insert a (maxChain r))

a ∈ insert a (maxChain r)
      α: Type u_1

β: Type ?u.2259

r: α → α → Prop

c: Set α

h: ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub

trans: ∀ {a b c : α}, r a b → r b c → r a c

this✝: ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub

ub: α

hub: ∀ (a : α), a ∈ maxChain r → r a ub

a: α

ha: r ub a

this: IsChain r (insert a (maxChain r))

a ∈ maxChain rexact mem_insert: ∀ {α : Type ?u.2848} (x : α) (s : Set α), x ∈ insert x s
mem_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 m
exists_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 m
exists_maximal_of_nonempty_chains_bounded [Nonempty: Sort ?u.2912 → Prop
Nonempty α: Type ?u.2897
α]
    (h: ∀ (c : Set α), IsChain r c → Set.Nonempty c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
h : ∀ c: ?m.2916
c, IsChain: {α : Type ?u.2920} → (α → α → Prop) → Set α → Prop
IsChain r: α → α → Prop
r c: ?m.2916
c → c: ?m.2916
c.Nonempty: {α : Type ?u.2931} → Set α → Prop
Nonempty → ∃ ub: ?m.2939
ub, ∀ a: ?m.2942
a ∈ c: ?m.2916
c, a: ?m.2942
a ≺ ub: ?m.2939
ub)
    (trans: ∀ {a b c : α}, r a b → r b c → r a c
trans : ∀ {a: ?m.2987
a b: ?m.2990
b c: ?m.2993
c}, a: ?m.2987
a ≺ b: ?m.2990
b → b: ?m.2990
b ≺ c: ?m.2993
c → a: ?m.2987
a ≺ c: ?m.2993
c) : ∃ m: ?m.3005
m, ∀ a: ?m.3008
a, m: ?m.3005
m ≺ a: ?m.3008
a → a: ?m.3008
a ≺ m: ?m.3005
m :=
  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 m
exists_maximal_of_chains_bounded
    (fun c: ?m.3037
c hc: ?m.3040
hc =>
      (eq_empty_or_nonempty: ∀ {α : Type ?u.3042} (s : Set α), s = ∅ ∨ Set.Nonempty s
eq_empty_or_nonempty c: ?m.3037
c).elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim
        (fun h: ?m.3059
h => ⟨Classical.arbitrary: (α : Sort ?u.3072) → [h : Nonempty α] → α
Classical.arbitrary α: Type ?u.2897
α, fun x: ?m.3087
x hx: ?m.3090
hx => (h: ?m.3059
h ▸ hx: ?m.3090
hx : x: ?m.3087
x ∈ (∅: ?m.3113
∅ : Set: Type ?u.3111 → Type ?u.3111
Set α: Type ?u.2897
α)).elim: ∀ {C : Sort ?u.3171}, False → C
elim⟩) (h: ∀ (c : Set α), IsChain r c → Set.Nonempty c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
h c: ?m.3037
c hc: ?m.3040
hc))
    trans: ∀ {a b c : α}, r a b → r b c → r a c
trans
#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 m
exists_maximal_of_nonempty_chains_bounded

section Preorder

variable [Preorder: Type ?u.3266 → Type ?u.3266
Preorder α: Type ?u.3251
α]

theorem zorn_preorder: (∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c) → ∃ m, ∀ (a : α), m ≤ a → a ≤ m
zorn_preorder (h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c
h : ∀ c: Set α
c : Set: Type ?u.3288 → Type ?u.3288
Set α: Type ?u.3269
α, IsChain: {α : Type ?u.3292} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: Set α
c → BddAbove: {α : Type ?u.3353} → [inst : Preorder α] → Set α → Prop
BddAbove c: Set α
c) :
    ∃ m: α
m : α: Type ?u.3269
α, ∀ a: ?m.3385
a, m: α
m ≤ a: ?m.3385
a → a: ?m.3385
a ≤ 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 m
exists_maximal_of_chains_bounded h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c
h le_trans: ∀ {α : Type ?u.3454} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_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 ≤ m
zorn_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 ≤ m
zorn_nonempty_preorder [Nonempty: Sort ?u.3528 → Prop
Nonempty α: Type ?u.3510
α]
    (h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → BddAbove c
h : ∀ c: Set α
c : Set: Type ?u.3532 → Type ?u.3532
Set α: Type ?u.3510
α, IsChain: {α : Type ?u.3536} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: Set α
c → c: Set α
c.Nonempty: {α : Type ?u.3598} → Set α → Prop
Nonempty → BddAbove: {α : Type ?u.3603} → [inst : Preorder α] → Set α → Prop
BddAbove c: Set α
c) : ∃ m: α
m : α: Type ?u.3510
α, ∀ a: ?m.3636
a, m: α
m ≤ a: ?m.3636
a → a: ?m.3636
a ≤ 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 m
exists_maximal_of_nonempty_chains_bounded h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → BddAbove c
h le_trans: ∀ {α : Type ?u.3754} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_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 ≤ m
zorn_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 ≤ m
zorn_preorder₀ (s: Set α
s : Set: Type ?u.3843 → Type ?u.3843
Set α: 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 ≤ ub
ih : ∀ (c: ?m.3847
c) (_: c ⊆ s
_ : c: ?m.3847
c ⊆ s: Set α
s), IsChain: {α : Type ?u.3869} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: ?m.3847
c → ∃ ub: ?m.3932
ub ∈ s: Set α
s, ∀ z: ?m.3953
z ∈ c: ?m.3847
c, z: ?m.3953
z ≤ ub: ?m.3932
ub) :
    ∃ m: ?m.4009
m ∈ s: Set α
s, ∀ z: ?m.4028
z ∈ s: Set α
s, m: ?m.4009
m ≤ z: ?m.4028
z → z: ?m.4028
z ≤ m: ?m.4009
m :=
  let ⟨⟨m: α
m, hms: m ∈ s
hms⟩, 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 ≤ m
zorn_preorder s: Set α
s _ fun c: ?m.4217
c hc: ?m.4220
hc =>
      let ⟨ub: α
ub, hubs: ub ∈ s
hubs, hub: ∀ (z : α), z ∈ Subtype.val '' c → z ≤ ub
hub⟩ :=
        ih: ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
ih (Subtype.val: {α : Sort ?u.4228} → {p : α → Prop} → Subtype p → α
Subtype.val '' c: ?m.4217
c) (fun _: ?m.4242
_ ⟨⟨_: α
_, hx: val✝ ∈ s
hx⟩, _, h: ↑{ val := val✝, property := hx } = x✝¹
h⟩ => h: ↑{ val := val✝, property := hx } = x✝¹
h ▸ hx: val✝ ∈ s
hx)
          (by
Goals accomplished! 🐙
            α: Type u_1

β: Type ?u.3828

r: α → α → Prop

c✝: 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 ≤ ub

c: Set ↑s

hc: IsChain (fun x x_1 => x ≤ x_1) c

IsChain (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 ∈ c
hpc⟨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 ∈ c
hqc⟨q, hqc, rfl⟩: q ∈ c ∧ ↑q = y✝
, rfl: ↑q = y✝
rfl⟨q, hqc, rfl⟩: q ∈ c ∧ ↑q = y✝
⟩ hpq: ↑p ≠ ↑q
hpqα: Type u_1

β: Type ?u.3828

r: α → α → Prop

c✝: 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 ≤ ub

c: Set ↑s

hc: IsChain (fun x x_1 => x ≤ x_1) c

p: { x // x ∈ s }

hpc: p ∈ c

q: { x // x ∈ s }

hqc: q ∈ c

hpq: ↑p ≠ ↑q

intro.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.3828

r: α → α → Prop

c✝: 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 ≤ ub

c: Set ↑s

hc: IsChain (fun x x_1 => x ≤ x_1) c

IsChain (fun x x_1 => x ≤ x_1) (Subtype.val '' c)refine' hc: IsChain (fun x x_1 => x ≤ x_1) c
hc hpc: p ∈ c
hpc hqc: q ∈ c
hqc fun t: ?m.5408
t => hpq: ↑p ≠ ↑q
hpq (Subtype.ext_iff: ∀ {α : Sort ?u.5410} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 t: ?m.5408
t)
Goals accomplished! 🐙)
      ⟨⟨ub: α
ub, hubs: ub ∈ s
hubs⟩, fun ⟨y: α
y, hy: y ∈ s
hy⟩ hc: ?m.4590
hc => hub: ∀ (z : α), z ∈ Subtype.val '' c → z ≤ ub
hub _: α
_ ⟨_: ?m.4660
_, hc: { val := y, property := hy } ∈ c
hc, rfl: ∀ {α : Sort ?u.4682} {a : α}, a = a
rfl⟩⟩
  ⟨m: α
m, hms: m ∈ s
hms, fun z: ?m.5062
z hzs: ?m.5065
hzs hmz: ?m.5068
hmz => h: ∀ (a : ↑s), { val := m, property := hms } ≤ a → a ≤ { val := m, property := hms }
h ⟨z: ?m.5062
z, hzs: ?m.5065
hzs⟩ hmz: ?m.5068
hmz⟩
#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 ≤ m
zorn_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 ≤ m
zorn_nonempty_preorder₀ (s: Set α
s : Set: Type ?u.5549 → Type ?u.5549
Set α: 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 ≤ ub
ih : ∀ (c: ?m.5553
c) (_: c ⊆ s
_ : c: ?m.5553
c ⊆ s: Set α
s), IsChain: {α : Type ?u.5575} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: ?m.5553
c → ∀ y: ?m.5636
y ∈ c: ?m.5553
c, ∃ ub: ?m.5674
ub ∈ s: Set α
s, ∀ z: ?m.5693
z ∈ c: ?m.5553
c, z: ?m.5693
z ≤ ub: ?m.5674
ub) (x: α
x : α: Type ?u.5531
α)
    (hxs: x ∈ s
hxs : x: α
x ∈ s: Set α
s) : ∃ m: ?m.5779
m ∈ s: Set α
s, x: α
x ≤ m: ?m.5779
m ∧ ∀ z: ?m.5801
z ∈ s: Set α
s, m: ?m.5779
m ≤ z: ?m.5801
z → z: ?m.5801
z ≤ m: ?m.5779
m := by
Goals 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.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ mhave H: ?m.5863
H := 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 ≤ m
zorn_preorder₀ ({ y: ?m.5872
y ∈ s: Set α
s | x: α
x ≤ y: ?m.5872
y }) fun c: ?m.5912
c hcs: ?m.5915
hcs hc: ?m.5918
hc => ?_: ∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : ?m.5865), z ∈ c → z ≤ ub
?_α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

H: ∃ m, m ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m

refine_2∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub
  α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m.α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

H: ∃ m, m ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m

refine_2∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

H: ∃ m, m ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m

refine_2∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ubrcases H: ?m.5863
H with ⟨m, ⟨hms, hxm⟩, hm⟩: ?m.5863
⟨m: α
m⟨m, ⟨hms, hxm⟩, hm⟩: ?m.5863
, ⟨hms, hxm⟩: m ∈ { y | y ∈ s ∧ x ≤ y }
⟨hms: m ∈ s
hms⟨hms, hxm⟩: m ∈ { y | y ∈ s ∧ x ≤ y }
, hxm: x ≤ m
hxm⟨hms, hxm⟩: m ∈ { y | y ∈ s ∧ x ≤ y }
⟩⟨m, ⟨hms, hxm⟩, hm⟩: ?m.5863
, hm: ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m
hm⟨m, ⟨hms, hxm⟩, hm⟩: ?m.5863
⟩α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

m: α

hm: ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m

hms: m ∈ s

hxm: x ≤ m

refine_2.intro.intro.intro∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
    α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

H: ∃ m, m ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m

refine_2∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ mexact ⟨m: α
m, hms: m ∈ s
hms, hxm: x ≤ m
hxm, fun z: ?m.6042
z hzs: ?m.6045
hzs hmz: ?m.6048
hmz => hm: ∀ (z : α), z ∈ { y | y ∈ s ∧ x ≤ y } → m ≤ z → z ≤ m
hm _: α
_ ⟨hzs: ?m.6045
hzs, hxm: x ≤ m
hxm.trans: ∀ {α : Type ?u.6061} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans hmz: ?m.6048
hmz⟩ hmz: ?m.6048
hmz⟩
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m·α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ubrcases c: ?m.5912
c.eq_empty_or_nonempty: ∀ {α : Type ?u.6077} (s : Set α), s = ∅ ∨ Set.Nonempty s
eq_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 ∈ c
hy⟨y, hy⟩: Set.Nonempty c
⟩(rfl | ⟨y, hy⟩): c = ∅ ∨ Set.Nonempty c
)α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

hcs: ∅ ⊆ { 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.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

refine_1.inr.intro∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub
    α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub·α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

hcs: ∅ ⊆ { 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.5534

r: α → α → Prop

c: 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 ≤ ub

x: α

hxs: x ∈ s

hcs: ∅ ⊆ { 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.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

refine_1.inr.intro∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ubexact ⟨x: α
x, ⟨hxs: x ∈ s
hxs, le_rfl: ∀ {α : Type ?u.6179} [inst : Preorder α] {a : α}, a ≤ a
le_rfl⟩, fun z: ?m.6197
z => False.elim: ∀ {C : Sort ?u.6199}, False → C
False.elim⟩
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

refine_1∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub·α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

refine_1.inr.intro∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

refine_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 ≤ ub
ih c: ?m.5912
c (fun z: ?m.6209
z hz: ?m.6212
hz => (hcs: ?m.5915
hcs hz: ?m.6212
hz).1: ∀ {a b : Prop}, a ∧ b → a
1) hc: ?m.5918
hc y: α
y hy: y ∈ c
hy 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 ∈ s
hzs⟨z, hzs, hz⟩: ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
, hz: ∀ (z_1 : α), z_1 ∈ c → z_1 ≤ z
hz⟨z, hzs, hz⟩: ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
⟩α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

z: α

hzs: z ∈ s

hz: ∀ (z_1 : α), z_1 ∈ c → z_1 ≤ z

refine_1.inr.intro.intro.intro∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ub
      α: Type u_1

β: Type ?u.5534

r: α → α → Prop

c✝: 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 ≤ ub

x: α

hxs: x ∈ s

c: Set α

hcs: c ⊆ { y | y ∈ s ∧ x ≤ y }

hc: IsChain (fun x x_1 => x ≤ x_1) c

y: α

hy: y ∈ c

refine_1.inr.intro∃ ub, ub ∈ { y | y ∈ s ∧ x ≤ y } ∧ ∀ (z : α), z ∈ c → z ≤ ubexact ⟨z: α
z, ⟨hzs: z ∈ s
hzs, (hcs: ?m.5915
hcs hy: y ∈ c
hy).2: ∀ {a b : Prop}, a ∧ b → b
2.trans: ∀ {α : Type ?u.6304} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| hz: ∀ (z_1 : α), z_1 ∈ c → z_1 ≤ z
hz _: α
_ hy: y ∈ c
hy⟩, hz: ∀ (z_1 : α), z_1 ∈ c → z_1 ≤ z
hz⟩
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 ≤ m
zorn_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 ≤ m
zorn_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 ≤ ub
ih : ∀ (c: ?m.6435
c) (_: c ⊆ Ici a
_ : c: ?m.6435
c ⊆ Ici: {α : Type ?u.6446} → [inst : Preorder α] → α → Set α
Ici a: α
a), IsChain: {α : Type ?u.6479} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: ?m.6435
c → ∀ y: ?m.6540
y ∈ c: ?m.6435
c, ∃ ub: ?m.6578
ub, a: α
a ≤ ub: ?m.6578
ub ∧ ∀ z: ?m.6592
z ∈ c: ?m.6435
c, z: ?m.6592
z ≤ ub: ?m.6578
ub)
    (x: α
x : α: Type ?u.6414
α) (hax: a ≤ x
hax : a: α
a ≤ x: α
x) : ∃ m: ?m.6645
m, x: α
x ≤ m: ?m.6645
m ∧ ∀ z: ?m.6651
z, m: ?m.6645
m ≤ z: ?m.6651
z → z: ?m.6651
z ≤ m: ?m.6645
m :=
  let ⟨m: α
m, _, hxm: x ≤ m
hxm, hm: ∀ (z : α), z ∈ Ici a → m ≤ z → z ≤ m
hm⟩ := 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 ≤ m
zorn_nonempty_preorder₀ (Ici: {α : Type ?u.6682} → [inst : Preorder α] → α → Set α
Ici a: α
a) (by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.6417

r: α → α → Prop

c: 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 ≤ ub

x: α

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 ≤ ub
ih
Goals accomplished! 🐙) x: α
x hax: a ≤ x
hax
  ⟨m: α
m, hxm: x ≤ m
hxm, fun z: ?m.6829
z hmz: ?m.6832
hmz => hm: ∀ (z : α), z ∈ Ici a → m ≤ z → z ≤ m
hm _: α
_ (hax: a ≤ x
hax.trans: ∀ {α : Type ?u.6839} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| hxm: x ≤ m
hxm.trans: ∀ {α : Type ?u.6854} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans hmz: ?m.6832
hmz) hmz: ?m.6832
hmz⟩
#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 ≤ m
zorn_nonempty_Ici₀

end Preorder

section PartialOrder

variable [PartialOrder: Type ?u.14751 → Type ?u.14751
PartialOrder α: Type ?u.14718
α]

theorem zorn_partialOrder: (∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c) → ∃ m, ∀ (a : α), m ≤ a → a = m
zorn_partialOrder (h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c
h : ∀ c: Set α
c : Set: Type ?u.14755 → Type ?u.14755
Set α: Type ?u.14736
α, IsChain: {α : Type ?u.14759} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: Set α
c → BddAbove: {α : Type ?u.14820} → [inst : Preorder α] → Set α → Prop
BddAbove c: Set α
c) :
    ∃ m: α
m : α: Type ?u.14736
α, ∀ a: ?m.14866
a, m: α
m ≤ a: ?m.14866
a → a: ?m.14866
a = m: α
m :=
  let ⟨m: α
m, hm: ∀ (a : α), m ≤ a → a ≤ m
hm⟩ := 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 ≤ m
zorn_preorder h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c
h
  ⟨m: α
m, fun a: ?m.15018
a ha: ?m.15021
ha => le_antisymm: ∀ {α : Type ?u.15023} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (hm: ∀ (a : α), m ≤ a → a ≤ m
hm a: ?m.15018
a ha: ?m.15021
ha) ha: ?m.15021
ha⟩
#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 = m
zorn_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 = m
zorn_nonempty_partialOrder [Nonempty: Sort ?u.15208 → Prop
Nonempty α: Type ?u.15190
α]
    (h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → BddAbove c
h : ∀ c: Set α
c : Set: Type ?u.15212 → Type ?u.15212
Set α: Type ?u.15190
α, IsChain: {α : Type ?u.15216} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: Set α
c → c: Set α
c.Nonempty: {α : Type ?u.15278} → Set α → Prop
Nonempty → BddAbove: {α : Type ?u.15283} → [inst : Preorder α] → Set α → Prop
BddAbove c: Set α
c) : ∃ m: α
m : α: Type ?u.15190
α, ∀ a: ?m.15330
a, m: α
m ≤ a: ?m.15330
a → a: ?m.15330
a = m: α
m :=
  let ⟨m: α
m, hm: ∀ (a : α), m ≤ a → a ≤ m
hm⟩ := 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 ≤ m
zorn_nonempty_preorder h: ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → BddAbove c
h
  ⟨m: α
m, fun a: ?m.15503
a ha: ?m.15506
ha => le_antisymm: ∀ {α : Type ?u.15508} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (hm: ∀ (a : α), m ≤ a → a ≤ m
hm a: ?m.15503
a ha: ?m.15506
ha) ha: ?m.15506
ha⟩
#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 = m
zorn_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 = m
zorn_partialOrder₀ (s: Set α
s : Set: Type ?u.15684 → Type ?u.15684
Set α: 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 ≤ ub
ih : ∀ (c: ?m.15688
c) (_: c ⊆ s
_ : c: ?m.15688
c ⊆ s: Set α
s), IsChain: {α : Type ?u.15710} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: ?m.15688
c → ∃ ub: ?m.15773
ub ∈ s: Set α
s, ∀ z: ?m.15794
z ∈ c: ?m.15688
c, z: ?m.15794
z ≤ ub: ?m.15773
ub) :
    ∃ m: ?m.15861
m ∈ s: Set α
s, ∀ z: ?m.15880
z ∈ s: Set α
s, m: ?m.15861
m ≤ z: ?m.15880
z → z: ?m.15880
z = m: ?m.15861
m :=
  let ⟨m: α
m, hms: m ∈ s
hms, hm: ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
hm⟩ := 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 ≤ m
zorn_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 ≤ ub
ih
  ⟨m: α
m, hms: m ∈ s
hms, fun z: ?m.16087
z hzs: ?m.16090
hzs hmz: ?m.16093
hmz => (hm: ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
hm z: ?m.16087
z hzs: ?m.16090
hzs hmz: ?m.16093
hmz).antisymm: ∀ {α : Type ?u.16095} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
antisymm hmz: ?m.16093
hmz⟩
#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 = m
zorn_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 = m
zorn_nonempty_partialOrder₀ (s: Set α
s : Set: Type ?u.16343 → Type ?u.16343
Set α: 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 ≤ ub
ih : ∀ (c: ?m.16347
c) (_: c ⊆ s
_ : c: ?m.16347
c ⊆ s: Set α
s), IsChain: {α : Type ?u.16369} → (α → α → Prop) → Set α → Prop
IsChain (· ≤ ·): α → α → Prop
(· ≤ ·) c: ?m.16347
c → ∀ y: ?m.16430
y ∈ c: ?m.16347
c, ∃ ub: ?m.16468
ub ∈ s: Set α
s, ∀ z: ?m.16487
z ∈ c: ?m.16347
c, z: ?m.16487
z ≤ ub: ?m.16468
ub) (x: α
x : α: Type ?u.16325
α)
    (hxs: x ∈ s
hxs : x: α
x ∈ s: Set α
s) : ∃ m: ?m.16584
m ∈ s: Set α
s, x: α
x ≤ m: ?m.16584
m ∧ ∀ z: ?m.16606
z ∈ s: Set α
s, m: ?m.16584
m ≤ z: ?m.16606
z → z: ?m.16606
z = m: ?m.16584
m :=
  let ⟨m: α
m, hms: m ∈ s
hms, hxm: x ≤ m
hxm, hm: ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
hm⟩ := 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 ≤ m
zorn_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 ≤ ub
ih x: α
x hxs: x ∈ s
hxs
  ⟨m: α
m, hms: m ∈ s
hms, hxm: x ≤ m
hxm, fun z: ?m.16841
z hzs: ?m.16844
hzs hmz: ?m.16847
hmz => (hm: ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
hm z: ?m.16841
z hzs: ?m.16844
hzs hmz: ?m.16847
hmz).antisymm: ∀ {α : Type ?u.16849} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
antisymm hmz: ?m.16847
hmz⟩
#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 = m
zorn_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 = m
zorn_subset (S: Set (Set α)
S : Set: Type ?u.17133 → Type ?u.17133
Set (Set: Type ?u.17134 → Type ?u.17134
Set α: 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 ⊆ ub
h : ∀ (c: ?m.17138
c) (_: c ⊆ S
_ : c: ?m.17138
c ⊆ S: Set (Set α)
S), IsChain: {α : Type ?u.17160} → (α → α → Prop) → Set α → Prop
IsChain (· ⊆ ·): Set α → Set α → Prop
(· ⊆ ·) c: ?m.17138
c → ∃ ub: ?m.17189
ub ∈ S: Set (Set α)
S, ∀ s: ?m.17210
s ∈ c: ?m.17138
c, s: ?m.17210
s ⊆ ub: ?m.17189
ub) :
    ∃ m: ?m.17266
m ∈ S: Set (Set α)
S, ∀ a: ?m.17285
a ∈ S: Set (Set α)
S, m: ?m.17266
m ⊆ a: ?m.17285
a → a: ?m.17285
a = m: ?m.17266
m :=
  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 = m
zorn_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 ⊆ ub
h
#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 = m
zorn_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 = m
zorn_subset_nonempty (S: Set (Set α)
S : Set: Type ?u.17464 → Type ?u.17464
Set (Set: Type ?u.17465 → Type ?u.17465
Set α: 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 ⊆ ub
H : ∀ (c: ?m.17469
c) (_: c ⊆ S
_ : c: ?m.17469
c ⊆ S: Set (Set α)
S), IsChain: {α : Type ?u.17491} → (α → α → Prop) → Set α → Prop
IsChain (· ⊆ ·): Set α → Set α → Prop
(· ⊆ ·) c: ?m.17469
c → c: ?m.17469
c.Nonempty: {α : Type ?u.17518} → Set α → Prop
Nonempty → ∃ ub: ?m.17526
ub ∈ S: Set (Set α)
S, ∀ s: ?m.17547
s ∈ c: ?m.17469
c, s: ?m.17547
s ⊆ ub: ?m.17526
ub) (x: Set α
x)
    (hx: x ∈ S
hx : x: ?m.17600
x ∈ S: Set (Set α)
S) : ∃ m: ?m.17636
m ∈ S: Set (Set α)
S, x: ?m.17600
x ⊆ m: ?m.17636
m ∧ ∀ a: ?m.17660
a ∈ S: Set (Set α)
S, m: ?m.17636
m ⊆ a: ?m.17660
a → a: ?m.17660
a = m: ?m.17636
m :=
  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 = m
zorn_nonempty_partialOrder₀ _: Set ?m.17728
_ (fun _: ?m.17732
_ cS: ?m.17735
cS hc: ?m.17738
hc y: ?m.17741
y yc: ?m.17744
yc => 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 ⊆ ub
H _: Set (Set α)
_ cS: ?m.17735
cS hc: ?m.17738
hc ⟨y: ?m.17741
y, yc: ?m.17744
yc⟩) _: ?m.17728
_ hx: x ∈ S
hx
#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 = m
zorn_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 = m
zorn_superset (S: Set (Set α)
S : Set: Type ?u.17904 → Type ?u.17904
Set (Set: Type ?u.17905 → Type ?u.17905
Set α: 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 ⊆ s
h : ∀ (c: ?m.17909
c) (_: c ⊆ S
_ : c: ?m.17909
c ⊆ S: Set (Set α)
S), IsChain: {α : Type ?u.17931} → (α → α → Prop) → Set α → Prop
IsChain (· ⊆ ·): Set α → Set α → Prop
(· ⊆ ·) c: ?m.17909
c → ∃ lb: ?m.17960
lb ∈ S: Set (Set α)
S, ∀ s: ?m.17981
s ∈ c: ?m.17909
c, lb: ?m.17960
lb ⊆ s: ?m.17981
s) :
    ∃ m: ?m.18037
m ∈ S: Set (Set α)
S, ∀ a: ?m.18056
a ∈ S: Set (Set α)
S, a: ?m.18056
a ⊆ m: ?m.18037
m → a: ?m.18056
a = m: ?m.18037
m :=
  (@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 = m
zorn_partialOrder₀ (Set: Type ?u.18123 → Type ?u.18123
Set α: Type ?u.17889
α)ᵒᵈ _ S: Set (Set α)
S) fun c: ?m.18194
c cS: ?m.18197
cS hc: ?m.18200
hc => h: ∀ (c : Set (Set α)), c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set α), s ∈ c → lb ⊆ s
h c: ?m.18194
c cS: ?m.18197
cS hc: ?m.18200
hc.symm: ∀ {α : Type ?u.18211} {r : α → α → Prop} {s : Set α}, IsChain r s → IsChain (flip r) s
symm
#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 = m
zorn_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 = m
zorn_superset_nonempty (S: Set (Set α)
S : Set: Type ?u.18293 → Type ?u.18293
Set (Set: Type ?u.18294 → Type ?u.18294
Set α: 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 ⊆ s
H : ∀ (c: ?m.18298
c) (_: c ⊆ S
_ : c: ?m.18298
c ⊆ S: Set (Set α)
S), IsChain: {α : Type ?u.18320} → (α → α → Prop) → Set α → Prop
IsChain (· ⊆ ·): Set α → Set α → Prop
(· ⊆ ·) c: ?m.18298
c → c: ?m.18298
c.Nonempty: {α : Type ?u.18347} → Set α → Prop
Nonempty → ∃ lb: ?m.18355
lb ∈ S: Set (Set α)
S, ∀ s: ?m.18376
s ∈ c: ?m.18298
c, lb: ?m.18355
lb ⊆ s: ?m.18376
s) (x: Set α
x)
    (hx: x ∈ S
hx : x: ?m.18429
x ∈ S: Set (Set α)
S) : ∃ m: ?m.18465
m ∈ S: Set (Set α)
S, m: ?m.18465
m ⊆ x: ?m.18429
x ∧ ∀ a: ?m.18489
a ∈ S: Set (Set α)
S, a: ?m.18489
a ⊆ m: ?m.18465
m → a: ?m.18489
a = m: ?m.18465
m :=
  @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 = m
zorn_nonempty_partialOrder₀ (Set: Type ?u.18558 → Type ?u.18558
Set α: Type ?u.18278
α)ᵒᵈ _ S: Set (Set α)
S (fun _: ?m.18563
_ cS: ?m.18566
cS hc: ?m.18569
hc y: ?m.18572
y yc: ?m.18575
yc => 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 ⊆ s
H _: Set (Set α)
_ cS: ?m.18566
cS hc: ?m.18569
hc.symm: ∀ {α : Type ?u.18655} {r : α → α → Prop} {s : Set α}, IsChain r s → IsChain (flip r) s
symm ⟨y: ?m.18572
y, yc: ?m.18575
yc⟩) _: (Set α)ᵒᵈ
_ hx: x ∈ S
hx
#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 = m
zorn_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 ⊆ M
IsChain.exists_maxChain (hc: IsChain r c
hc : IsChain: {α : Type ?u.18766} → (α → α → Prop) → Set α → Prop
IsChain r: α → α → Prop
r c: Set α
c) : ∃ M: ?m.18781
M, @IsMaxChain: {α : Type ?u.18783} → (α → α → Prop) → Set α → Prop
IsMaxChain _: Type ?u.18783
_ r: α → α → Prop
r M: ?m.18781
M ∧ c: Set α
c ⊆ M: ?m.18781
M := by
Goals 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.
  -- obtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩ :=
  --   zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } _ c ⟨Subset.rfl, hc⟩
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ Mhave H: ?m.18809
H := 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 = m
zorn_subset_nonempty { s: ?m.18817
s | c: Set α
c ⊆ s: ?m.18817
s ∧ IsChain: {α : Type ?u.18831} → (α → α → Prop) → Set α → Prop
IsChain r: α → α → Prop
r s: ?m.18817
s } ?_: ∀ (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 ⊆ s
Subset.rfl, hc: IsChain r c
hc⟩α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

H: ∃ m, m ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ m ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → m ⊆ a → a = m

refine_2∃ M, IsMaxChain r M ∧ c ⊆ M
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

refine_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.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ M·α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

H: ∃ m, m ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ m ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → m ⊆ a → a = m

refine_2∃ M, IsMaxChain r M ∧ c ⊆ M α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

H: ∃ m, m ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ m ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → m ⊆ a → a = m

refine_2∃ M, IsMaxChain r M ∧ c ⊆ M
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

refine_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 ⊆ ubobtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩: M ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ M ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
⟨M: Set α
M⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩: M ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ M ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
, ⟨_, hM₀⟩: M ∈ { s | c ⊆ s ∧ IsChain r s }
⟨_: c ⊆ M
_⟨_, hM₀⟩: M ∈ { s | c ⊆ s ∧ IsChain r s }
, hM₀: IsChain r M
hM₀⟨_, hM₀⟩: M ∈ { s | c ⊆ s ∧ IsChain r s }
⟩⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩: M ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ M ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
, hM₁: c ⊆ M
hM₁⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩: M ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ M ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
, hM₂: ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
hM₂⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩: M ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ M ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
⟩ := H: ?m.18809
Hα: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

M: Set α

left✝: c ⊆ M

hM₀: IsChain r M

hM₁: c ⊆ M

hM₂: ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M

refine_2.intro.intro.intro.intro∃ M, IsMaxChain r M ∧ c ⊆ M
    α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

H: ∃ m, m ∈ { s | c ⊆ s ∧ IsChain r s } ∧ c ⊆ m ∧ ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → m ⊆ a → a = m

refine_2∃ M, IsMaxChain r M ∧ c ⊆ Mexact ⟨M: Set α
M, ⟨hM₀: IsChain r M
hM₀, fun d: ?m.18978
d hd: ?m.18981
hd hMd: ?m.18984
hMd => (hM₂: ∀ (a : Set α), a ∈ { s | c ⊆ s ∧ IsChain r s } → M ⊆ a → a = M
hM₂ _: Set α
_ ⟨hM₁: c ⊆ M
hM₁.trans: ∀ {α : Type ?u.18993} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
trans hMd: ?m.18984
hMd, hd: ?m.18981
hd⟩ hMd: ?m.18984
hMd).symm: ∀ {α : Sort ?u.19033} {a b : α}, a = b → b = a
symm⟩, hM₁: c ⊆ M
hM₁⟩
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: 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) cs
hcs₁ ⟨s, hs⟩: Set.Nonempty cs
⟨s: Set α
s⟨s, hs⟩: Set.Nonempty cs
, hs: s ∈ cs
hs⟨s, hs⟩: Set.Nonempty cs
⟩α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

refine_1.intro∃ ub, ub ∈ { s | c ⊆ s ∧ IsChain r s } ∧ ∀ (s : Set α), s ∈ cs → s ⊆ ub
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ Mrefine'
    ⟨⋃₀cs: Set (Set ?m.18811)
cs, ⟨fun _: ?m.19109
_ ha: ?m.19112
ha => Set.mem_sUnion_of_mem: ∀ {α : Type ?u.19114} {x : α} {t : Set α} {S : Set (Set α)}, x ∈ t → t ∈ S → x ∈ ⋃₀ S
Set.mem_sUnion_of_mem ((hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }
hcs₀ hs: s ∈ cs
hs).left: ∀ {a b : Prop}, a ∧ b → a
left ha: ?m.19112
ha) hs: s ∈ cs
hs, _: ?m.19107
_⟩, fun _: ?m.19136
_ =>
      Set.subset_sUnion_of_mem: ∀ {α : Type ?u.19138} {S : Set (Set α)} {t : Set α}, t ∈ S → t ⊆ ⋃₀ S
Set.subset_sUnion_of_mem⟩α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

refine_1.introIsChain r (⋃₀ cs)
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: 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 ∈ cs
hsy⟨sy, hsy, hysy⟩: y ∈ ⋃₀ cs
, hysy: y ∈ sy
hysy⟨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 ∈ cs
hsz⟨sz, hsz, hzsz⟩: sz ∈ cs ∧ z ∈ sz
, hzsz: z ∈ sz
hzsz⟨sz, hsz, hzsz⟩: sz ∈ cs ∧ z ∈ sz
⟩ hyz: y ≠ z
hyzα: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

refine_1.intro.intro.intro.intro.intror y z ∨ r z y
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ Mobtain rfl: sy = sz
rflrfl | hsseq: sy = sz ∨ sy ≠ sz
 | hsseq: sy ≠ sz
hsseq := eq_or_ne: ∀ {α : Sort ?u.19244} (x y : α), x = y ∨ x ≠ y
eq_or_ne sy: Set α
sy sz: Set α
szα: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

hyz: y ≠ z

hsz: sy ∈ cs

hzsz: z ∈ sy

refine_1.intro.intro.intro.intro.intro.inlr y z ∨ r z y
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

refine_1.intro.intro.intro.intro.intro.inrr y z ∨ r z y
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ M·α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

hyz: y ≠ z

hsz: sy ∈ cs

hzsz: z ∈ sy

refine_1.intro.intro.intro.intro.intro.inlr y z ∨ r z y α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

hyz: y ≠ z

hsz: sy ∈ cs

hzsz: z ∈ sy

refine_1.intro.intro.intro.intro.intro.inlr y z ∨ r z y
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

refine_1.intro.intro.intro.intro.intro.inrr y z ∨ r z yexact (hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }
hcs₀ hsy: sy ∈ cs
hsy).right: ∀ {a b : Prop}, a ∧ b → b
right hysy: y ∈ sy
hysy hzsz: z ∈ sy
hzsz hyz: y ≠ z
hyz
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ Mcases' hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs
hcs₁ hsy: sy ∈ cs
hsy hsz: sz ∈ cs
hsz hsseq: sy ≠ sz
hsseq with h: ?m.19340
h h: ?m.19341
hα: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sy sz

refine_1.intro.intro.intro.intro.intro.inr.inlr y z ∨ r z y
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sz sy

refine_1.intro.intro.intro.intro.intro.inr.inrr y z ∨ r z y
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ M·α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sy sz

refine_1.intro.intro.intro.intro.intro.inr.inlr y z ∨ r z y α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sy sz

refine_1.intro.intro.intro.intro.intro.inr.inlr y z ∨ r z y
α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sz sy

refine_1.intro.intro.intro.intro.intro.inr.inrr y z ∨ r z yexact (hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }
hcs₀ hsz: sz ∈ cs
hsz).right: ∀ {a b : Prop}, a ∧ b → b
right (h: ?m.19340
h hysy: y ∈ sy
hysy) hzsz: z ∈ sz
hzsz hyz: y ≠ z
hyz
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

∃ M, IsMaxChain r M ∧ c ⊆ M·α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sz sy

refine_1.intro.intro.intro.intro.intro.inr.inrr y z ∨ r z y α: Type u_1

β: Type ?u.18754

r: α → α → Prop

c: Set α

hc: IsChain r c

cs: Set (Set α)

hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }

hcs₁: IsChain (fun x x_1 => x ⊆ x_1) cs

s: Set α

hs: s ∈ cs

y: α

sy: Set α

hsy: sy ∈ cs

hysy: y ∈ sy

z: α

sz: Set α

hsz: sz ∈ cs

hzsz: z ∈ sz

hyz: y ≠ z

hsseq: sy ≠ sz

h: (fun x x_1 => x ⊆ x_1) sz sy

refine_1.intro.intro.intro.intro.intro.inr.inrr y z ∨ r z yexact (hcs₀: cs ⊆ { s | c ⊆ s ∧ IsChain r s }
hcs₀ hsy: sy ∈ cs
hsy).right: ∀ {a b : Prop}, a ∧ b → b
right hysy: y ∈ sy
hysy (h: ?m.19341
h hzsz: z ∈ sz
hzsz) hyz: y ≠ z
hyz
Goals 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 ⊆ M
IsChain.exists_maxChain