-- Mathlib/Order/ZornAtoms.lean
theorem IsCoatomic.of_isChain_bounded {α : Type*} [PartialOrder α] [OrderTop α]
    (h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → ⊤ ∉ c → ∃ x ≠ ⊤, x ∈ upperBounds c) :
    IsCoatomic α

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 => x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False

Tactic:
exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ m, x ≤ m ∧ Maximal (fun x_1 => x_1 ∈ Ico x ⊤) m
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
obtain ⟨y, hxy, hmax⟩ := this

Result:
case refine_2.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 => x_1 ∈ Ico x ⊤) y
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 => x_1 ∈ Ico x ⊤) y
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩

Result:
case refine_2.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 => x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩

Result:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hz : z ≠ ⊤
hcz : z ∈ upperBounds c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α

Tactic:
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)

Result:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ m, x ≤ m ∧ Maximal (fun x_1 => x_1 ∈ Ico x ⊤) m
⊢ ∃ a, IsCoatom a ∧ x ≤ a

case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub