case refine_2
α : Type u_1
β : Type ?u.5559
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

case refine_1
α : Type u_1
β : Type ?u.5559
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
α : Type u_1
β : Type ?u.5559
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
have H := zorn_preorder₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_
case refine_1
α : Type u_1
β : Type ?u.5559
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
case refine_2
α : Type u_1
β : Type ?u.5559
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

case refine_1
α : Type u_1
β : Type ?u.5559
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
. rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
  exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
case refine_2.intro.intro.intro
α : Type u_1
β : Type ?u.5559
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
case refine_2
α : Type u_1
β : Type ?u.5559
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
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
no goals
case refine_2.intro.intro.intro
α : Type u_1
β : Type ?u.5559
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
exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
case refine_1.inl
α : Type u_1
β : Type ?u.5559
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

case refine_1.inr.intro
α : Type u_1
β : Type ?u.5559
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
case refine_1
α : Type u_1
β : Type ?u.5559
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
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
no goals
case refine_1.inl
α : Type u_1
β : Type ?u.5559
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
exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
case refine_1.inr.intro.intro.intro
α : Type u_1
β : Type ?u.5559
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
case refine_1.inr.intro
α : Type u_1
β : Type ?u.5559
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
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
no goals
case refine_1.inr.intro.intro.intro
α : Type u_1
β : Type ?u.5559
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
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩