-- Mathlib/Order/Zorn.lean
theorem zorn_le_nonempty₀ (s : Set α)
    (ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α) (hxs : x ∈ s) :
    ∃ m, x ≤ m ∧ Maximal (· ∈ s) m

Proof state:
case refine_1.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) ∅
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ ∅, z ≤ ub

Tactic:
exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, Maximal (fun x_1 => x_1 ∈ {y | y ∈ s ∧ x ≤ y}) m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m

Tactic:
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun x_1 => x_1 ∈ {y | y ∈ s ∧ x ≤ y}) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun x_1 => x_1 ∈ {y | y ∈ s ∧ x ≤ y}) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m

Tactic:
exact ⟨m, hxm, hms, fun z hzs hmz => @hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩

Result:
no goals

Proof state:
case refine_1.inr.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Result:
no goals

Proof state:
case refine_1.inr.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩

Result:
case refine_1.inr.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Proof state:
case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)

Result:
case refine_1.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) ∅
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ ∅, z ≤ ub

case refine_1.inr.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
⊢ ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m

Tactic:
have H := zorn_le₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_

Result:
case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, Maximal (fun x_1 => x_1 ∈ {y | y ∈ s ∧ x ≤ y}) m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m

case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub