From de5038953210a6ffb013340c7bf82243be226f1c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 31 Mar 2022 17:21:48 +0000
Subject: [PATCH] split(order/chain): Split off `order.zorn` (#13060)

Split `order.zorn` into two files, one about chains, the other one about Zorn's lemma.
---
 src/order/chain.lean | 221 ++++++++++++++++++++++++++++++++++++++++
 src/order/zorn.lean  | 238 +------------------------------------------
 2 files changed, 225 insertions(+), 234 deletions(-)
 create mode 100644 src/order/chain.lean

diff --git a/src/order/chain.lean b/src/order/chain.lean
new file mode 100644
index 0000000000000..626ce0e35f20f
--- /dev/null
+++ b/src/order/chain.lean
@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import data.set.pairwise
+
+/-!
+# Chains
+
+This file defines chains for an arbitrary relation and proves Hausdorff's Maximality Principle.
+
+## Main declarations
+
+* `is_chain s`: A chain `s` is a set of comparable elements.
+* `max_chain_spec`: Hausdorff's Maximality Principle.
+
+## Notes
+
+Originally ported from Isabelle/HOL. The
+[original file](https://isabelle.in.tum.de/dist/library/HOL/HOL/Zorn.html) was written by Jacques D.
+Fleuriot, Tobias Nipkow, Christian Sternagel.
+-/
+
+open classical set
+
+variables {α β : Type*} (r : α → α → Prop)
+
+local infix ` ≺ `:50 := r
+
+section chain
+variables (r)
+
+/-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
+def is_chain (s : set α) : Prop := s.pairwise (λ x y, x ≺ y ∨ y ≺ x)
+
+/-- `super_chain s t` means that `t` is a chain that strictly includes `s`. -/
+def super_chain (s t : set α) : Prop := is_chain r t ∧ s ⊂ t
+
+/-- A chain `s` is a maximal chain if there does not exists a chain strictly including `s`. -/
+def is_max_chain (s : set α) : Prop := is_chain r s ∧ ∀ ⦃t⦄, is_chain r t → s ⊆ t → s = t
+
+variables {r} {c c₁ c₂ c₃ s t : set α} {a b x y : α}
+
+lemma is_chain_empty : is_chain r ∅ := set.pairwise_empty _
+
+lemma set.subsingleton.is_chain (hs : s.subsingleton) : is_chain r s := hs.pairwise _
+
+lemma is_chain.mono : s ⊆ t → is_chain r t → is_chain r s := set.pairwise.mono
+
+/-- This can be used to turn `is_chain (≥)` into `is_chain (≤)` and vice-versa. -/
+lemma is_chain.symm (h : is_chain r s) : is_chain (flip r) s := h.mono' $ λ _ _, or.symm
+
+lemma is_chain_of_trichotomous [is_trichotomous α r] (s : set α) : is_chain r s :=
+λ a _ b _ hab, (trichotomous_of r a b).imp_right $ λ h, h.resolve_left hab
+
+lemma is_chain.insert (hs : is_chain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b ∨ b ≺ a) :
+  is_chain r (insert a s) :=
+hs.insert_of_symmetric (λ _ _, or.symm) ha
+
+lemma is_chain_univ_iff : is_chain r (univ : set α) ↔ is_trichotomous α r :=
+begin
+  refine ⟨λ h, ⟨λ a b , _⟩, λ h, @is_chain_of_trichotomous _ _ h univ⟩,
+  rw [or.left_comm, or_iff_not_imp_left],
+  exact h trivial trivial,
+end
+
+lemma is_chain.image (r : α → α → Prop) (s : β → β → Prop) (f : α → β)
+  (h : ∀ x y, r x y → s (f x) (f y)) {c : set α} (hrc : is_chain r c) :
+  is_chain s (f '' c) :=
+λ x ⟨a, ha₁, ha₂⟩ y ⟨b, hb₁, hb₂⟩, ha₂ ▸ hb₂ ▸ λ hxy,
+  (hrc ha₁ hb₁ $ ne_of_apply_ne f hxy).imp (h _ _) (h _ _)
+
+section total
+variables [is_refl α r]
+
+lemma is_chain.total (h : is_chain r s) (hx : x ∈ s) (hy : y ∈ s) : x ≺ y ∨ y ≺ x :=
+(eq_or_ne x y).elim (λ e, or.inl $ e ▸ refl _) (h hx hy)
+
+lemma is_chain.directed_on (H : is_chain r s) : directed_on r s :=
+λ x hx y hy, (H.total hx hy).elim (λ h, ⟨y, hy, h, refl _⟩) $ λ h, ⟨x, hx, refl _, h⟩
+
+protected lemma is_chain.directed {f : β → α} {c : set β} (h : is_chain (f ⁻¹'o r) c) :
+  directed r (λ x : {a : β // a ∈ c}, f x) :=
+λ ⟨a, ha⟩ ⟨b, hb⟩, by_cases
+  (λ hab : a = b, by simp only [hab, exists_prop, and_self, subtype.exists];
+    exact ⟨b, hb, refl _⟩) $
+  λ hab, (h ha hb hab).elim (λ h, ⟨⟨b, hb⟩, h, refl _⟩) $ λ h, ⟨⟨a, ha⟩, refl _, h⟩
+
+end total
+
+lemma is_max_chain.is_chain (h : is_max_chain r s) : is_chain r s := h.1
+lemma is_max_chain.not_super_chain (h : is_max_chain r s) : ¬super_chain r s t :=
+λ ht, ht.2.ne $ h.2 ht.1 ht.2.1
+
+open_locale classical
+
+/-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `succ_chain s`
+is one of these chains. Otherwise it is `s`. -/
+def succ_chain (r : α → α → Prop) (s : set α) : set α :=
+if h : ∃ t, is_chain r s ∧ super_chain r s t then some h else s
+
+lemma succ_chain_spec (h : ∃ t, is_chain r s ∧ super_chain r s t) :
+  super_chain r s (succ_chain r s) :=
+let ⟨t, hc'⟩ := h in
+have is_chain r s ∧ super_chain r s (some h),
+  from @some_spec _ (λ t, is_chain r s ∧ super_chain r s t) _,
+by simp [succ_chain, dif_pos, h, this.right]
+
+lemma is_chain.succ (hs : is_chain r s) : is_chain r (succ_chain r s) :=
+if h : ∃ t, is_chain r s ∧ super_chain r s t then (succ_chain_spec h).1
+  else by { simp [succ_chain, dif_neg, h], exact hs }
+
+lemma is_chain.super_chain_succ_chain (hs₁ : is_chain r s) (hs₂ : ¬ is_max_chain r s) :
+  super_chain r s (succ_chain r s) :=
+begin
+  simp [is_max_chain, not_and_distrib, not_forall_not] at hs₂,
+  obtain ⟨t, ht, hst⟩ := hs₂.neg_resolve_left hs₁,
+  exact succ_chain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩,
+end
+
+lemma subset_succ_chain : s ⊆ succ_chain r s :=
+if h : ∃ t, is_chain r s ∧ super_chain r s t then (succ_chain_spec h).2.1
+  else by simp [succ_chain, dif_neg, h, subset.rfl]
+
+/-- Predicate for whether a set is reachable from `∅` using `succ_chain` and `⋃₀`. -/
+inductive chain_closure (r : α → α → Prop) : set α → Prop
+| succ : ∀ {s}, chain_closure s → chain_closure (succ_chain r s)
+| union : ∀ {s}, (∀ a ∈ s, chain_closure a) → chain_closure (⋃₀ s)
+
+/-- An explicit maximal chain. `max_chain` is taken to be the union of all sets in `chain_closure`.
+-/
+def max_chain (r : α → α → Prop) := ⋃₀ set_of (chain_closure r)
+
+lemma chain_closure_empty : chain_closure r ∅ :=
+have chain_closure r (⋃₀ ∅),
+  from chain_closure.union $ λ a h, h.rec _,
+by simpa using this
+
+lemma chain_closure_max_chain : chain_closure r (max_chain r) := chain_closure.union $ λ s, id
+
+private lemma chain_closure_succ_total_aux (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
+  (h : ∀ ⦃c₃⦄, chain_closure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain r c₃ ⊆ c₂) :
+  succ_chain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂ :=
+begin
+  induction hc₁,
+  case succ : c₃ hc₃ ih
+  { cases ih with ih ih,
+    { exact or.inl (ih.trans subset_succ_chain) },
+    { exact (h hc₃ ih).imp_left (λ h, h ▸ subset.rfl) } },
+  case union : s hs ih
+  { refine (or_iff_not_imp_left.2 $ λ hn, sUnion_subset $ λ a ha, _),
+    exact (ih a ha).resolve_left (λ h, hn $ h.trans $ subset_sUnion_of_mem ha) }
+end
+
+private lemma chain_closure_succ_total (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
+  (h : c₁ ⊆ c₂) :
+  c₂ = c₁ ∨ succ_chain r c₁ ⊆ c₂ :=
+begin
+  induction hc₂ generalizing c₁ hc₁ h,
+  case succ : c₂ hc₂ ih
+  { refine (chain_closure_succ_total_aux hc₁ hc₂ $ λ c₁, ih).imp h.antisymm' (λ h₁, _),
+    obtain rfl | h₂ := ih hc₁ h₁,
+    { exact subset.rfl },
+    { exact h₂.trans subset_succ_chain } },
+  case union : s hs ih
+  { apply or.imp_left h.antisymm',
+    apply classical.by_contradiction,
+    simp [not_or_distrib, sUnion_subset_iff, not_forall],
+    intros c₃ hc₃ h₁ h₂,
+    obtain h | h := chain_closure_succ_total_aux hc₁ (hs c₃ hc₃) (λ c₄, ih _ hc₃),
+    { exact h₁ (subset_succ_chain.trans h) },
+    obtain h' | h' := ih c₃ hc₃ hc₁ h,
+    { exact h₁ h'.subset },
+    { exact h₂ (h'.trans $ subset_sUnion_of_mem hc₃) } }
+end
+
+lemma chain_closure.total (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) :
+  c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
+(chain_closure_succ_total_aux hc₂ hc₁ $ λ c₃ hc₃, chain_closure_succ_total hc₃ hc₁).imp_left
+  subset_succ_chain.trans
+
+lemma chain_closure.succ_fixpoint (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
+  (hc : succ_chain r c₂ = c₂) :
+  c₁ ⊆ c₂ :=
+begin
+  induction hc₁,
+  case succ : s₁ hc₁ h
+  { exact (chain_closure_succ_total hc₁ hc₂ h).elim (λ h, h ▸ hc.subset) id },
+  case union : s hs ih
+  { exact sUnion_subset ih }
+end
+
+lemma chain_closure.succ_fixpoint_iff (hc : chain_closure r c) :
+  succ_chain r c = c ↔ c = max_chain r :=
+⟨λ h, (subset_sUnion_of_mem hc).antisymm $ chain_closure_max_chain.succ_fixpoint hc h,
+  λ h, subset_succ_chain.antisymm' $ (subset_sUnion_of_mem hc.succ).trans h.symm.subset⟩
+
+lemma chain_closure.is_chain (hc : chain_closure r c) : is_chain r c :=
+begin
+  induction hc,
+  case succ : c hc h
+  { exact h.succ },
+  case union : s hs h
+  { change ∀ c ∈ s, is_chain r c at h,
+    exact λ c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq,
+      ((hs _ ht₁).total $ hs _ ht₂).elim
+        (λ ht, h t₂ ht₂ (ht hc₁) hc₂ hneq)
+        (λ ht, h t₁ ht₁ hc₁ (ht hc₂) hneq) }
+end
+
+/-- **Hausdorff's maximality principle**
+
+There exists a maximal totally ordered set of `α`.
+Note that we do not require `α` to be partially ordered by `r`. -/
+lemma max_chain_spec : is_max_chain r (max_chain r) :=
+classical.by_contradiction $ λ h,
+let ⟨h₁, H⟩ := chain_closure_max_chain.is_chain.super_chain_succ_chain h in
+  H.ne (chain_closure_max_chain.succ_fixpoint_iff.mpr rfl).symm
+
+end chain
diff --git a/src/order/zorn.lean b/src/order/zorn.lean
index 8374a88a38cde..c500a04929c33 100644
--- a/src/order/zorn.lean
+++ b/src/order/zorn.lean
@@ -3,19 +3,12 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import data.set.pairwise
+import order.chain
 
 /-!
-# Chains and Zorn's lemmas
+# Zorn's lemmas
 
-This file defines chains for an arbitrary relation and proves several formulations of Zorn's Lemma,
-along with Hausdorff's Maximality Principle.
-
-## Main declarations
-
-* `is_chain s`: A chain `s` is a set of comparable elements.
-* `max_chain_spec`: Hausdorff's Maximality Principle.
-* `exists_maximal_of_chains_bounded`: Zorn's Lemma. Many variants are offered.
+This file proves several formulations of Zorn's Lemma.
 
 ## Variants
 
@@ -67,233 +60,12 @@ Originally ported from Isabelle/HOL. The
 Fleuriot, Tobias Nipkow, Christian Sternagel.
 -/
 
-noncomputable theory
-
 open classical set
 
-variables {α β : Type*} (r : α → α → Prop)
+variables {α β : Type*} {r : α → α → Prop} {c : set α}
 
 local infix ` ≺ `:50  := r
 
-/-! ### Chains -/
-
-section chain
-variables (r)
-
-/-- A chain is a subset `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
-def is_chain (s : set α) := s.pairwise (λ x y, x ≺ y ∨ y ≺ x)
-
-/-- `super_chain s t` means that `t` is a chain that strictly includes `s`. -/
-def super_chain (s t : set α) : Prop := is_chain r t ∧ s ⊂ t
-
-/-- A chain `s` is a maximal chain if there does not exists a chain strictly including `s`. -/
-def is_max_chain (s : set α) := is_chain r s ∧ ∀ ⦃t⦄, is_chain r t → s ⊆ t → s = t
-
-variables {r} {c c₁ c₂ c₃ s t : set α} {a b x y : α}
-
-lemma is_chain_empty : is_chain r ∅ := set.pairwise_empty _
-
-lemma set.subsingleton.is_chain (hs : s.subsingleton) : is_chain r s := hs.pairwise _
-
-lemma is_chain.mono : s ⊆ t → is_chain r t → is_chain r s := set.pairwise.mono
-
-lemma is_chain.total [is_refl α r] (h : is_chain r s) (hx : x ∈ s) (hy : y ∈ s) : x ≺ y ∨ y ≺ x :=
-by { classical, exact if e : x = y then or.inl (e ▸ refl _) else h hx hy e }
-
-/-- This can be used to turn `is_chain (≥)` into `is_chain (≤)` and vice-versa. -/
-lemma is_chain.symm (h : is_chain r s) : is_chain (flip r) s := h.mono' $ λ _ _, or.symm
-
-lemma is_chain_of_trichotomous [is_trichotomous α r] (s : set α) : is_chain r s :=
-begin
-  intros a _ b _ hab,
-  obtain h | h | h := @trichotomous _ r _ a b,
-  { exact or.inl h },
-  { exact (hab h).elim },
-  { exact or.inr h }
-end
-
-lemma is_chain.insert (hs : is_chain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b ∨ b ≺ a) :
-  is_chain r (insert a s) :=
-hs.insert_of_symmetric (λ _ _, or.symm) ha
-
-lemma is_chain_univ_iff : is_chain r (univ : set α) ↔ is_trichotomous α r :=
-begin
-  refine ⟨λ h, ⟨λ a b , _⟩, λ h, @is_chain_of_trichotomous _ _ h univ⟩,
-  rw [or.left_comm, or_iff_not_imp_left],
-  exact h trivial trivial,
-end
-
-lemma is_chain.image (r : α → α → Prop) (s : β → β → Prop) (f : α → β)
-  (h : ∀ x y, r x y → s (f x) (f y)) {c : set α} (hrc : is_chain r c) :
-  is_chain s (f '' c) :=
-λ x ⟨a, ha₁, ha₂⟩ y ⟨b, hb₁, hb₂⟩, ha₂ ▸ hb₂ ▸ λ hxy,
-  (hrc ha₁ hb₁ $ ne_of_apply_ne f hxy).imp (h _ _) (h _ _)
-
-lemma is_chain.directed_on [is_refl α r] (H : is_chain r s) : directed_on (≺) s :=
-λ x hx y hy,
-match H.total hx hy with
-| or.inl h := ⟨y, hy, h, refl _⟩
-| or.inr h := ⟨x, hx, refl _, h⟩
-end
-
-lemma is_chain.directed {r} [is_refl β r] {f : α → β} {c : set α} (h : is_chain (f ⁻¹'o r) c) :
-  directed r (λ x : {a : α // a ∈ c}, f x) :=
-λ ⟨a, ha⟩ ⟨b, hb⟩, by_cases
-  (λ hab : a = b, by simp only [hab, exists_prop, and_self, subtype.exists];
-    exact ⟨b, hb, refl _⟩)
-  (λ hab, (h ha hb hab).elim
-    (λ h : r (f a) (f b), ⟨⟨b, hb⟩, h, refl _⟩)
-    (λ h : r (f b) (f a), ⟨⟨a, ha⟩, refl _, h⟩))
-
-lemma is_max_chain.is_chain (h : is_max_chain r s) : is_chain r s := h.1
-lemma is_max_chain.not_super_chain (h : is_max_chain r s) : ¬super_chain r s t :=
-λ ht, ht.2.ne $ h.2 ht.1 ht.2.1
-
-open_locale classical
-
-/-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `succ_chain s`
-is one of these chains. Otherwise it is `s`. -/
-def succ_chain (r : α → α → Prop) (s : set α) : set α :=
-if h : ∃ t, is_chain r s ∧ super_chain r s t then some h else s
-
-lemma succ_spec (h : ∃ t, is_chain r s ∧ super_chain r s t) : super_chain r s (succ_chain r s) :=
-let ⟨t, hc'⟩ := h in
-have is_chain r s ∧ super_chain r s (some h),
-  from @some_spec _ (λ t, is_chain r s ∧ super_chain r s t) _,
-by simp [succ_chain, dif_pos, h, this.right]
-
-lemma is_chain.succ (hs : is_chain r s) :  is_chain r (succ_chain r s) :=
-if h : ∃ t, is_chain r s ∧ super_chain r s t then
-  (succ_spec h).left
-else
-  by simp [succ_chain, dif_neg, h]; exact hs
-
-lemma is_chain.super_chain_succ_chain (hs₁ : is_chain r s) (hs₂ : ¬ is_max_chain r s) :
-  super_chain r s (succ_chain r s) :=
-begin
-  simp [is_max_chain, not_and_distrib, not_forall_not] at hs₂,
-  obtain ⟨t, ht, hst⟩ := hs₂.neg_resolve_left hs₁,
-  exact succ_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩,
-end
-
-lemma succ_increasing {s : set α} : s ⊆ succ_chain r s :=
-if h : ∃ t, is_chain r s ∧ super_chain r s t then
-  have super_chain r s (succ_chain r s), from succ_spec h,
-  this.right.left
-else by simp [succ_chain, dif_neg, h, subset.refl]
-
-/-- Predicate for whether a set is reachable from `∅` using `succ_chain` and `⋃₀`. -/
-inductive chain_closure (r : α → α → Prop) : set α → Prop
-| succ : ∀ {s}, chain_closure s → chain_closure (succ_chain r s)
-| union : ∀ {s}, (∀ a ∈ s, chain_closure a) → chain_closure (⋃₀ s)
-
-/-- An explicit maximal chain. `max_chain` is taken to be the union of all sets in `chain_closure`.
--/
-def max_chain (r : α → α → Prop) := ⋃₀ set_of (chain_closure r)
-
-lemma chain_closure_empty : chain_closure r ∅ :=
-have chain_closure r (⋃₀ ∅),
-  from chain_closure.union $ λ a h, h.rec _,
-by simpa using this
-
-lemma chain_closure_max_chain : chain_closure r (max_chain r) := chain_closure.union $ λ s, id
-
-private lemma chain_closure_succ_total_aux (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
-  (h : ∀ {c₃}, chain_closure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain r c₃ ⊆ c₂) :
-  c₁ ⊆ c₂ ∨ succ_chain r c₂ ⊆ c₁ :=
-begin
-  induction hc₁,
-  case succ : c₃ hc₃ ih
-  { cases ih with ih ih,
-    { exact (h hc₃ ih).symm.imp_right (λ h, h ▸ subset.rfl) },
-    { exact or.inr (subset.trans ih succ_increasing) } },
-  case union : s hs ih
-  { refine (or_iff_not_imp_right.2 $ λ hn, sUnion_subset $ λ a ha, _),
-    exact (ih a ha).resolve_right (λ h, hn $ h.trans $ subset_sUnion_of_mem ha) }
-end
-
-private lemma chain_closure_succ_total (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
-  (h : c₁ ⊆ c₂) :
-  c₂ = c₁ ∨ succ_chain r c₁ ⊆ c₂ :=
-begin
-  induction hc₂ generalizing c₁ hc₁ h,
-  case succ : c₂ hc₂ ih
-  { have h₁ : c₁ ⊆ c₂ ∨ succ_chain r c₂ ⊆ c₁ :=
-      (chain_closure_succ_total_aux hc₁ hc₂ $ λ c₁, ih),
-    cases h₁ with h₁ h₁,
-    { have h₂ := ih hc₁ h₁,
-      cases h₂ with h₂ h₂,
-      { exact (or.inr $ h₂ ▸ subset.refl _) },
-      { exact (or.inr $ subset.trans h₂ succ_increasing) } },
-    { exact (or.inl $ subset.antisymm h₁ h) } },
-  case union : s hs ih
-  { apply or.imp_left (λ h', subset.antisymm h' h),
-    apply classical.by_contradiction,
-    simp [not_or_distrib, sUnion_subset_iff, not_forall],
-    intros c₃ hc₃ h₁ h₂,
-    have h := chain_closure_succ_total_aux hc₁ (hs c₃ hc₃) (λ c₄, ih _ hc₃),
-    cases h with h h,
-    { have h' := ih c₃ hc₃ hc₁ h,
-      cases h' with h' h',
-      { exact h₁ h'.subset },
-      { exact h₂ (h'.trans $ subset_sUnion_of_mem hc₃) } },
-    { exact h₁ (succ_increasing.trans  h) } }
-end
-
-lemma chain_closure_total (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) :
-  c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
-or.imp_right succ_increasing.trans $ chain_closure_succ_total_aux hc₁ hc₂ $ λ c₃ hc₃,
-  chain_closure_succ_total hc₃ hc₂
-
-lemma chain_closure.succ_fixpoint (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂)
-  (h_eq : succ_chain r c₂ = c₂) :
-  c₁ ⊆ c₂ :=
-begin
-  induction hc₁,
-  case succ : s₁ hc₁ h
-  { exact (chain_closure_succ_total hc₁ hc₂ h).elim (λ h, h ▸ h_eq.subset) id },
-  case union : s hs ih
-  { exact (sUnion_subset $ λ s₁ hc₁, ih s₁ hc₁) }
-end
-
-lemma chain_closure.succ_fixpoint_iff (hc : chain_closure r c) :
-  succ_chain r c = c ↔ c = max_chain r :=
-⟨λ h, (subset_sUnion_of_mem hc).antisymm (chain_closure_max_chain.succ_fixpoint hc h), λ h,
-  subset.antisymm
-    (calc succ_chain r c ⊆ ⋃₀ {c : set α | chain_closure r c} : subset_sUnion_of_mem hc.succ
-      ... = c : h.symm)
-    succ_increasing⟩
-
-lemma chain_closure.is_chain (hc : chain_closure r c) : is_chain r c :=
-begin
-  induction hc,
-  case succ : c hc h
-  { exact h.succ },
-  case union : s hs h
-  { have h : ∀ c ∈ s, is_chain r c := h,
-    exact λ c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq,
-      have t₁ ⊆ t₂ ∨ t₂ ⊆ t₁, from chain_closure_total (hs _ ht₁) (hs _ ht₂),
-      or.elim this
-        (λ ht, h t₂ ht₂ (ht hc₁) hc₂ hneq)
-        (λ ht, h t₁ ht₁ hc₁ (ht hc₂) hneq) }
-end
-
-/-- **Hausdorff's maximality principle**
-
-There exists a maximal totally ordered subset of `α`.
-Note that we do not require `α` to be partially ordered by `r`. -/
-lemma max_chain_spec : is_max_chain r (max_chain r) :=
-classical.by_contradiction $ λ h,
-let ⟨h₁, H⟩ := chain_closure_max_chain.is_chain.super_chain_succ_chain h in
-  H.ne (chain_closure_max_chain.succ_fixpoint_iff.mpr rfl).symm
-
-end chain
-
-/-! ### Zorn's lemma -/
-
-section zorn
-variables {r} {c : set α}
-
 /-- **Zorn's lemma**
 
 If every chain has an upper bound, then there exists a maximal element. -/
@@ -400,5 +172,3 @@ begin
   { exact (hcs₀ hsz).right (h hysy) hzsz hyz },
   { exact (hcs₀ hsy).right hysy (h hzsz) hyz }
 end
-
-end zorn