[GOAL]
α : Type u_1
β : Type u_2
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 r
[PROOFSTEP]
rw [maxChain_spec.right this (subset_insert _ _)]
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact mem_insert _ _
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
⊢ (fun x x_1 => x ≤ x_1) ↑p ↑q ∨ (fun x x_1 => x ≤ x_1) ↑q ↑p
[PROOFSTEP]
refine' hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have H := zorn_preorder₀ ({y ∈ s | x ≤ y}) fun c hcs hc => ?_
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
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
⊢ ∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
[PROOFSTEP]
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
[GOAL]
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
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
⊢ ∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
[PROOFSTEP]
exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
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
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
[GOAL]
case refine_1.inl
α : Type u_1
β : Type u_2
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) ∅
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ ∅ → z ≤ ub
[PROOFSTEP]
exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
[GOAL]
case refine_1.inr.intro
α : Type u_1
β : Type u_2
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
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
[GOAL]
case refine_1.inr.intro.intro.intro
α : Type u_1
β : Type u_2
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
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩
[GOAL]
α : Type u_1
β : Type u_2
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 ≤ ub
[PROOFSTEP]
simpa using ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
have H := zorn_subset_nonempty {s | c ⊆ s ∧ IsChain r s} ?_ c ⟨Subset.rfl, hc⟩
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
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
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
obtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩ := H
[GOAL]
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
exact ⟨M, ⟨hM₀, fun d hd hMd => (hM₂ _ ⟨hM₁.trans hMd, hd⟩ hMd).symm⟩, hM₁⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ (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
[PROOFSTEP]
rintro cs hcs₀ hcs₁ ⟨s, hs⟩
[GOAL]
case refine_1.intro
α : Type u_1
β : Type u_2
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
⊢ ∃ ub, ub ∈ {s | c ⊆ s ∧ IsChain r s} ∧ ∀ (s : Set α), s ∈ cs → s ⊆ ub
[PROOFSTEP]
refine' ⟨⋃₀ cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, _⟩, fun _ => Set.subset_sUnion_of_mem⟩
[GOAL]
case refine_1.intro
α : Type u_1
β : Type u_2
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
⊢ IsChain r (⋃₀ cs)
[PROOFSTEP]
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
⊢ r y z ∨ r z y
[PROOFSTEP]
obtain rfl | hsseq := eq_or_ne sy sz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
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
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsy).right hysy hzsz hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
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
⊢ r y z ∨ r z y
[PROOFSTEP]
cases' hcs₁ hsy hsz hsseq with h h
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
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
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsz).right (h hysy) hzsz hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
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
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsy).right hysy (h hzsz) hyz
