-- Mathlib/Order/Zorn.lean
theorem IsChain.exists_maxChain (hc : IsChain r c) : ∃ M, @IsMaxChain _ r M ∧ c ⊆ M

Proof state:
case refine_2
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H : ∃ m, c ⊆ m ∧ Maximal (fun x => x ∈ {s | c ⊆ s ∧ IsChain r s}) m
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
obtain ⟨M, hcM, hM⟩ := H

Result:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
M : Set α
hcM : c ⊆ M
hM : Maximal (fun x => x ∈ {s | c ⊆ s ∧ IsChain r s}) M
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Proof state:
case refine_1.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ IsChain r (⋃₀ cs)

Tactic:
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz

Result:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

Proof state:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
M : Set α
hcM : c ⊆ M
hM : Maximal (fun x => x ∈ {s | c ⊆ s ∧ IsChain r s}) M
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩

Result:
case refine_2
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H : ∃ m, c ⊆ m ∧ Maximal (fun x => x ∈ {s | c ⊆ s ∧ IsChain r s}) m
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s},
    IsChain (fun x1 x2 => x1 ⊆ x2) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub

Proof state:
case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

Tactic:
rcases hcs₁ hsy hsz hsseq with h | h

Result:
case refine_1.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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 : sy ⊆ sz
⊢ r y z ∨ r z y

case refine_1.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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 : sz ⊆ sy
⊢ r y z ∨ r z y

Proof state:
case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s},
    IsChain (fun x1 x2 => x1 ⊆ x2) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub

Tactic:
rintro cs hcs₀ hcs₁ ⟨s, hs⟩

Result:
case refine_1.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ cs, s ⊆ ub

Proof state:
case refine_1.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ cs, s ⊆ ub

Tactic:
refine
  ⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
    Set.subset_sUnion_of_mem⟩

Result:
case refine_1.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ IsChain r (⋃₀ cs)

Proof state:
case refine_1.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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 : sy ⊆ sz
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsz).right (h hysy) hzsz hyz

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

Tactic:
obtain rfl | hsseq := eq_or_ne sy sz

Result:
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

Proof state:
case refine_1.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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 : sz ⊆ sy
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsy).right hysy (h hzsz) hyz

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 => x1 ⊆ x2) 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

Tactic:
exact (hcs₀ hsy).right hysy hzsz hyz

Result:
no goals