[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
⊢ IsCoatomic α
[PROOFSTEP]
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
have : ∃ y ∈ Ico x ⊤, x ≤ y ∧ ∀ z ∈ Ico x ⊤, y ≤ z → z = y :=
  by
  refine zorn_nonempty_partialOrder₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
  rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
  exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ y, y ∈ Ico x ⊤ ∧ x ≤ y ∧ ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
[PROOFSTEP]
refine zorn_nonempty_partialOrder₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
⊢ ∃ ub, ub ∈ Ico x ⊤ ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub, ub ∈ Ico x ⊤ ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ y, y ∈ Ico x ⊤ ∧ x ≤ y ∧ ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
rcases this with ⟨y, ⟨hxy, hy⟩, -, hy'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hy : y < ⊤
hy' : ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
⊢ ∃ a, IsCoatom a ∧ x ≤ a
[PROOFSTEP]
refine ⟨y, ⟨hy.ne, fun z hyz => le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ¬⊤ ∈ c → ∃ x x_1, x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hy : y < ⊤
hy' : ∀ (z : α), z ∈ Ico x ⊤ → y ≤ z → z = y
z : α
hyz : y < z
hz : z < ⊤
⊢ False
[PROOFSTEP]
exact hyz.ne' (hy' z ⟨hxy.trans hyz.le, hz⟩ hyz.le)
