---input---
/-
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

Zorn's lemmas.

Ported from Isabelle/HOL (written by Jacques D. Fleuriot, Tobias Nipkow, and Christian Sternagel).
-/
import data.set.lattice
noncomputable theory

universes u
open set classical
local attribute [instance] decidable_inhabited
local attribute [instance] prop_decidable

namespace zorn

section chain
parameters {α : Type u} {r : α → α → Prop}
local infix ` ≺ `:50  := r

def chain (c : set α) := pairwise_on c (λx y, x ≺ y ∨ y ≺ x)

theorem chain_insert {c : set α} {a : α} (hc : chain c) (ha : ∀b∈c, b ≠ a → a ≺ b ∨ b ≺ a) :
  chain (insert a c) :=
forall_insert_of_forall
  (assume x hx, forall_insert_of_forall (hc x hx) (assume hneq, (ha x hx hneq).symm))
  (forall_insert_of_forall (assume x hx hneq, ha x hx $ assume h', hneq h'.symm) (assume h, (h rfl).rec _))

def super_chain (c₁ c₂ : set α) := chain c₂ ∧ c₁ ⊂ c₂

def is_max_chain (c : set α) := chain c ∧ ¬ (∃c', super_chain c c')

def succ_chain (c : set α) :=
if h : ∃c', chain c ∧ super_chain c c' then some h else c

theorem succ_spec {c : set α} (h : ∃c', chain c ∧ super_chain c c') :
  super_chain c (succ_chain c) :=
let ⟨c', hc'⟩ := h in
have chain c ∧ super_chain c (some h),
  from @some_spec _ (λc', chain c ∧ super_chain c c') _,
by simp [succ_chain, dif_pos, h, this.right]

theorem chain_succ {c : set α} (hc : chain c) : chain (succ_chain c) :=
if h : ∃c', chain c ∧ super_chain c c' then
  (succ_spec h).left
else
  by simp [succ_chain, dif_neg, h]; exact hc

theorem super_of_not_max {c : set α} (hc₁ : chain c) (hc₂ : ¬ is_max_chain c) :
  super_chain c (succ_chain c) :=
begin
  simp [is_max_chain, not_and_iff, not_not_iff] at hc₂,
  exact have ∃c', super_chain c c', from hc₂.neg_resolve_left hc₁,
  let ⟨c', hc'⟩ := this in
  show super_chain c (succ_chain c),
    from succ_spec ⟨c', hc₁, hc'⟩
end

theorem succ_increasing {c : set α} : c ⊆ succ_chain c :=
if h : ∃c', chain c ∧ super_chain c c' then
  have super_chain c (succ_chain c), from succ_spec h,
  this.right.left
else by simp [succ_chain, dif_neg, h, subset.refl]

inductive chain_closure : set α → Prop
| succ : ∀{s}, chain_closure s → chain_closure (succ_chain s)
| union : ∀{s}, (∀a∈s, chain_closure a) → chain_closure (⋃₀ s)

theorem chain_closure_empty : chain_closure ∅ :=
have chain_closure (⋃₀ ∅),
  from chain_closure.union $ assume a h, h.rec _,
by simp at this; assumption

theorem chain_closure_closure : chain_closure (⋃₀ chain_closure) :=
chain_closure.union $ assume s hs, hs

variables {c c₁ c₂ c₃ : set α}

private lemma chain_closure_succ_total_aux (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
  (h : ∀{c₃}, chain_closure c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain c₃ ⊆ c₂) :
  c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁ :=
begin
  induction hc₁,
  case _root_.zorn.chain_closure.succ c₃ hc₃ ih {
    cases ih with ih ih,
    { have h := h hc₃ ih,
      cases h with h h,
      { exact or.inr (h ▸ subset.refl _) },
      { exact or.inl h } },
    { exact or.inr (subset.trans ih succ_increasing) } },
  case _root_.zorn.chain_closure.union s hs ih {
    refine (or_of_not_implies' $ λ hn, sUnion_subset $ λ a ha, _),
    apply (ih a ha).resolve_right,
    apply mt (λ h, _) hn,
    exact subset.trans h (subset_sUnion_of_mem ha) }
end

private lemma chain_closure_succ_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) (h : c₁ ⊆ c₂) :
  c₂ = c₁ ∨ succ_chain c₁ ⊆ c₂ :=
begin
  induction hc₂ generalizing c₁ hc₁ h,
  case _root_.zorn.chain_closure.succ c₂ hc₂ ih {
    have h₁ : c₁ ⊆ c₂ ∨ @succ_chain α r c₂ ⊆ c₁ :=
      (chain_closure_succ_total_aux hc₁ hc₂ $ assume 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 _root_.zorn.chain_closure.union s hs ih {
    apply or.imp (assume h', subset.antisymm h' h) id,
    apply classical.by_contradiction,
    simp [not_or_iff, sUnion_subset_iff, classical.not_forall_iff, not_implies_iff],
    intro h, cases h with h₁ h₂, cases h₂ with c₃ h₂, cases h₂ with h₂ hc₃,
    have h := chain_closure_succ_total_aux hc₁ (hs c₃ hc₃) (assume c₄, ih _ hc₃),
    cases h with h h,
    { have h' := ih c₃ hc₃ hc₁ h,
      cases h' with h' h',
      { exact (h₂ $ h' ▸ subset.refl _) },
      { exact (h₁ $ subset.trans h' $ subset_sUnion_of_mem hc₃) } },
    { exact (h₂ $ subset.trans succ_increasing h) } }
end

theorem chain_closure_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
have c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁,
  from chain_closure_succ_total_aux hc₁ hc₂ $ assume c₃ hc₃, chain_closure_succ_total hc₃ hc₂,
or.imp_right (assume : succ_chain c₂ ⊆ c₁, subset.trans succ_increasing this) this

theorem chain_closure_succ_fixpoint (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
  (h_eq : succ_chain c₂ = c₂) : c₁ ⊆ c₂ :=
begin
  induction hc₁,
  case _root_.zorn.chain_closure.succ c₁ hc₁ h {
    exact or.elim (chain_closure_succ_total hc₁ hc₂ h)
      (assume h, h ▸ h_eq.symm ▸ subset.refl c₂) id },
  case _root_.zorn.chain_closure.union s hs ih {
    exact (sUnion_subset $ assume c₁ hc₁, ih c₁ hc₁) }
end

theorem chain_closure_succ_fixpoint_iff (hc : chain_closure c) :
  succ_chain c = c ↔ c = ⋃₀ chain_closure :=
⟨assume h, subset.antisymm
    (subset_sUnion_of_mem hc)
    (chain_closure_succ_fixpoint chain_closure_closure hc h),
  assume : c = ⋃₀{c : set α | chain_closure c},
  subset.antisymm
    (calc succ_chain c ⊆ ⋃₀{c : set α | chain_closure c} :
        subset_sUnion_of_mem $ chain_closure.succ hc
      ... = c : this.symm)
    succ_increasing⟩

theorem chain_chain_closure (hc : chain_closure c) : chain c :=
begin
  induction hc,
  case _root_.zorn.chain_closure.succ c hc h {
    exact chain_succ h },
  case _root_.zorn.chain_closure.union s hs h {
    have h : ∀c∈s, zorn.chain c := h,
    exact assume 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
        (assume : t₁ ⊆ t₂, h t₂ ht₂ c₁ (this hc₁) c₂ hc₂ hneq)
        (assume : t₂ ⊆ t₁, h t₁ ht₁ c₁ hc₁ c₂ (this hc₂) hneq) }
end

def max_chain := ⋃₀ chain_closure

/-- Hausdorff's maximality principle

There exists a maximal totally ordered subset of `α`.
Note that we do not require `α` to be partially ordered by `r`. -/
theorem max_chain_spec : is_max_chain max_chain :=
classical.by_contradiction $
assume : ¬ is_max_chain (⋃₀ chain_closure),
have super_chain (⋃₀ chain_closure) (succ_chain (⋃₀ chain_closure)),
  from super_of_not_max (chain_chain_closure chain_closure_closure) this,
let ⟨h₁, h₂, (h₃ : (⋃₀ chain_closure) ≠ succ_chain (⋃₀ chain_closure))⟩ := this in
have succ_chain (⋃₀ chain_closure) = (⋃₀ chain_closure),
  from (chain_closure_succ_fixpoint_iff chain_closure_closure).mpr rfl,
h₃ this.symm

/-- Zorn's lemma

If every chain has an upper bound, then there is a maximal element -/
theorem zorn (h : ∀c, chain c → ∃ub, ∀a∈c, a ≺ ub) (trans : ∀{a b c}, a ≺ b → b ≺ c → a ≺ c) :
  ∃m, ∀a, m ≺ a → a ≺ m :=
have ∃ub, ∀a∈max_chain, a ≺ ub,
  from h _ $ max_chain_spec.left,
let ⟨ub, (hub : ∀a∈max_chain, a ≺ ub)⟩ := this in
⟨ub, assume a ha,
  have chain (insert a max_chain),
    from chain_insert max_chain_spec.left $ assume b hb _, or.inr $ trans (hub b hb) ha,
  have a ∈ max_chain, from
    classical.by_contradiction $ assume h : a ∉ max_chain,
    max_chain_spec.right $ ⟨insert a max_chain, this, ssubset_insert h⟩,
  hub a this⟩

end chain

theorem zorn_weak_order {α : Type u} [weak_order α]
  (h : ∀c:set α, @chain α (≤) c → ∃ub, ∀a∈c, a ≤ ub) : ∃m:α, ∀a, m ≤ a → a = m :=
let ⟨m, hm⟩ := @zorn α (≤) h (assume a b c, le_trans) in
⟨m, assume a ha, le_antisymm (hm a ha) ha⟩

end zorn

---tokens---
'/-'          Comment
'\n'          Comment.Multiline

'C'           Comment.Multiline
'o'           Comment.Multiline
'p'           Comment.Multiline
'y'           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
'g'           Comment.Multiline
'h'           Comment.Multiline
't'           Comment.Multiline
' '           Comment.Multiline
'('           Comment.Multiline
'c'           Comment.Multiline
')'           Comment.Multiline
' '           Comment.Multiline
'2'           Comment.Multiline
'0'           Comment.Multiline
'1'           Comment.Multiline
'7'           Comment.Multiline
' '           Comment.Multiline
'J'           Comment.Multiline
'o'           Comment.Multiline
'h'           Comment.Multiline
'a'           Comment.Multiline
'n'           Comment.Multiline
'n'           Comment.Multiline
'e'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'H'           Comment.Multiline
'ö'           Comment.Multiline
'l'           Comment.Multiline
'z'           Comment.Multiline
'l'           Comment.Multiline
'.'           Comment.Multiline
' '           Comment.Multiline
'A'           Comment.Multiline
'l'           Comment.Multiline
'l'           Comment.Multiline
' '           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
'g'           Comment.Multiline
'h'           Comment.Multiline
't'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'r'           Comment.Multiline
'e'           Comment.Multiline
's'           Comment.Multiline
'e'           Comment.Multiline
'r'           Comment.Multiline
'v'           Comment.Multiline
'e'           Comment.Multiline
'd'           Comment.Multiline
'.'           Comment.Multiline
'\n'          Comment.Multiline

'R'           Comment.Multiline
'e'           Comment.Multiline
'l'           Comment.Multiline
'e'           Comment.Multiline
'a'           Comment.Multiline
's'           Comment.Multiline
'e'           Comment.Multiline
'd'           Comment.Multiline
' '           Comment.Multiline
'u'           Comment.Multiline
'n'           Comment.Multiline
'd'           Comment.Multiline
'e'           Comment.Multiline
'r'           Comment.Multiline
' '           Comment.Multiline
'A'           Comment.Multiline
'p'           Comment.Multiline
'a'           Comment.Multiline
'c'           Comment.Multiline
'h'           Comment.Multiline
'e'           Comment.Multiline
' '           Comment.Multiline
'2'           Comment.Multiline
'.'           Comment.Multiline
'0'           Comment.Multiline
' '           Comment.Multiline
'l'           Comment.Multiline
'i'           Comment.Multiline
'c'           Comment.Multiline
'e'           Comment.Multiline
'n'           Comment.Multiline
's'           Comment.Multiline
'e'           Comment.Multiline
' '           Comment.Multiline
'a'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'd'           Comment.Multiline
'e'           Comment.Multiline
's'           Comment.Multiline
'c'           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
'b'           Comment.Multiline
'e'           Comment.Multiline
'd'           Comment.Multiline
' '           Comment.Multiline
'i'           Comment.Multiline
'n'           Comment.Multiline
' '           Comment.Multiline
't'           Comment.Multiline
'h'           Comment.Multiline
'e'           Comment.Multiline
' '           Comment.Multiline
'f'           Comment.Multiline
'i'           Comment.Multiline
'l'           Comment.Multiline
'e'           Comment.Multiline
' '           Comment.Multiline
'L'           Comment.Multiline
'I'           Comment.Multiline
'C'           Comment.Multiline
'E'           Comment.Multiline
'N'           Comment.Multiline
'S'           Comment.Multiline
'E'           Comment.Multiline
'.'           Comment.Multiline
'\n'          Comment.Multiline

'A'           Comment.Multiline
'u'           Comment.Multiline
't'           Comment.Multiline
'h'           Comment.Multiline
'o'           Comment.Multiline
'r'           Comment.Multiline
's'           Comment.Multiline
':'           Comment.Multiline
' '           Comment.Multiline
'J'           Comment.Multiline
'o'           Comment.Multiline
'h'           Comment.Multiline
'a'           Comment.Multiline
'n'           Comment.Multiline
'n'           Comment.Multiline
'e'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'H'           Comment.Multiline
'ö'           Comment.Multiline
'l'           Comment.Multiline
'z'           Comment.Multiline
'l'           Comment.Multiline
'\n'          Comment.Multiline

'\n'          Comment.Multiline

'Z'           Comment.Multiline
'o'           Comment.Multiline
'r'           Comment.Multiline
'n'           Comment.Multiline
"'"           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'l'           Comment.Multiline
'e'           Comment.Multiline
'm'           Comment.Multiline
'm'           Comment.Multiline
'a'           Comment.Multiline
's'           Comment.Multiline
'.'           Comment.Multiline
'\n'          Comment.Multiline

'\n'          Comment.Multiline

'P'           Comment.Multiline
'o'           Comment.Multiline
'r'           Comment.Multiline
't'           Comment.Multiline
'e'           Comment.Multiline
'd'           Comment.Multiline
' '           Comment.Multiline
'f'           Comment.Multiline
'r'           Comment.Multiline
'o'           Comment.Multiline
'm'           Comment.Multiline
' '           Comment.Multiline
'I'           Comment.Multiline
's'           Comment.Multiline
'a'           Comment.Multiline
'b'           Comment.Multiline
'e'           Comment.Multiline
'l'           Comment.Multiline
'l'           Comment.Multiline
'e'           Comment.Multiline
'/'           Comment.Multiline
'H'           Comment.Multiline
'O'           Comment.Multiline
'L'           Comment.Multiline
' '           Comment.Multiline
'('           Comment.Multiline
'w'           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
't'           Comment.Multiline
't'           Comment.Multiline
'e'           Comment.Multiline
'n'           Comment.Multiline
' '           Comment.Multiline
'b'           Comment.Multiline
'y'           Comment.Multiline
' '           Comment.Multiline
'J'           Comment.Multiline
'a'           Comment.Multiline
'c'           Comment.Multiline
'q'           Comment.Multiline
'u'           Comment.Multiline
'e'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'D'           Comment.Multiline
'.'           Comment.Multiline
' '           Comment.Multiline
'F'           Comment.Multiline
'l'           Comment.Multiline
'e'           Comment.Multiline
'u'           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
'o'           Comment.Multiline
't'           Comment.Multiline
','           Comment.Multiline
' '           Comment.Multiline
'T'           Comment.Multiline
'o'           Comment.Multiline
'b'           Comment.Multiline
'i'           Comment.Multiline
'a'           Comment.Multiline
's'           Comment.Multiline
' '           Comment.Multiline
'N'           Comment.Multiline
'i'           Comment.Multiline
'p'           Comment.Multiline
'k'           Comment.Multiline
'o'           Comment.Multiline
'w'           Comment.Multiline
','           Comment.Multiline
' '           Comment.Multiline
'a'           Comment.Multiline
'n'           Comment.Multiline
'd'           Comment.Multiline
' '           Comment.Multiline
'C'           Comment.Multiline
'h'           Comment.Multiline
'r'           Comment.Multiline
'i'           Comment.Multiline
's'           Comment.Multiline
't'           Comment.Multiline
'i'           Comment.Multiline
'a'           Comment.Multiline
'n'           Comment.Multiline
' '           Comment.Multiline
'S'           Comment.Multiline
't'           Comment.Multiline
'e'           Comment.Multiline
'r'           Comment.Multiline
'n'           Comment.Multiline
'a'           Comment.Multiline
'g'           Comment.Multiline
'e'           Comment.Multiline
'l'           Comment.Multiline
')'           Comment.Multiline
'.'           Comment.Multiline
'\n'          Comment.Multiline

'-/'          Comment.Multiline
'\n'          Text

'import'      Keyword.Namespace
' '           Text
'data.set.lattice' Name
'\n'          Text

'noncomputable theory' Keyword.Declaration
'\n\n'        Text

'universes'   Keyword.Declaration
' '           Text
'u'           Name
'\n'          Text

'open'        Keyword.Namespace
' '           Text
'set'         Name
' '           Text
'classical'   Name
'\n'          Text

'local'       Keyword.Namespace
' '           Text
'attribute'   Keyword.Namespace
' '           Text
'['           Operator
'instance'    Keyword.Declaration
']'           Operator
' '           Text
'decidable_inhabited' Name
'\n'          Text

'local'       Keyword.Namespace
' '           Text
'attribute'   Keyword.Namespace
' '           Text
'['           Operator
'instance'    Keyword.Declaration
']'           Operator
' '           Text
'prop_decidable' Name
'\n\n'        Text

'namespace'   Keyword.Namespace
' '           Text
'zorn'        Name
'\n\n'        Text

'section'     Keyword.Namespace
' '           Text
'chain'       Name
'\n'          Text

'parameters'  Keyword.Declaration
' '           Text
'{'           Operator
'α'           Name
' '           Text
':'           Operator
' '           Text
'Type'        Keyword.Type
' '           Text
'u'           Name
'}'           Operator
' '           Text
'{'           Operator
'r'           Name
' '           Text
':'           Operator
' '           Text
'α'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'α'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'Prop'        Keyword.Type
'}'           Operator
'\n'          Text

'local'       Keyword.Namespace
' '           Text
'infix'       Keyword.Declaration
' '           Text
'`'           Name.Builtin.Pseudo
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'`'           Name.Builtin.Pseudo
':'           Operator
'50'          Literal.Number.Integer
'  '          Text
':='          Operator
' '           Text
'r'           Name
'\n\n'        Text

'def'         Keyword.Declaration
' '           Text
'chain'       Name
' '           Text
'('           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
')'           Operator
' '           Text
':='          Operator
' '           Text
'pairwise_on' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'λ'           Name.Builtin.Pseudo
'x'           Name
' '           Text
'y'           Name
','           Operator
' '           Text
'x'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'y'           Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'y'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'x'           Name
')'           Operator
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_insert' Name
' '           Text
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
' '           Text
'{'           Operator
'a'           Name
' '           Text
':'           Operator
' '           Text
'α'           Name
'}'           Operator
' '           Text
'('           Operator
'hc'          Name
' '           Text
':'           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
')'           Operator
' '           Text
'('           Operator
'ha'          Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'b'           Name
'∈'           Name.Builtin.Pseudo
'c'           Name
','           Operator
' '           Text
'b'           Name
' '           Text
'≠'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'b'           Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'b'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'a'           Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'chain'       Name
' '           Text
'('           Operator
'insert'      Name
' '           Text
'a'           Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'forall_insert_of_forall' Name
'\n  '        Text
'('           Operator
'assume'      Keyword
' '           Text
'x'           Name
' '           Text
'hx'          Name
','           Operator
' '           Text
'forall_insert_of_forall' Name
' '           Text
'('           Operator
'hc'          Name
' '           Text
'x'           Name
' '           Text
'hx'          Name
')'           Operator
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
'hneq'        Name
','           Operator
' '           Text
'('           Operator
'ha'          Name
' '           Text
'x'           Name
' '           Text
'hx'          Name
' '           Text
'hneq'        Name
')'           Operator
'.'           Name.Builtin.Pseudo
'symm'        Name
')'           Operator
')'           Operator
'\n  '        Text
'('           Operator
'forall_insert_of_forall' Name
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
'x'           Name
' '           Text
'hx'          Name
' '           Text
'hneq'        Name
','           Operator
' '           Text
'ha'          Name
' '           Text
'x'           Name
' '           Text
'hx'          Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
"h'"          Name
','           Operator
' '           Text
'hneq'        Name
' '           Text
"h'.symm"     Name
')'           Operator
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
'h'           Name
','           Operator
' '           Text
'('           Operator
'h'           Name
' '           Text
'rfl'         Name
')'           Operator
'.'           Name.Builtin.Pseudo
'rec'         Name
' '           Text
'_'           Name
')'           Operator
')'           Operator
'\n\n'        Text

'def'         Keyword.Declaration
' '           Text
'super_chain' Name
' '           Text
'('           Operator
'c₁'          Name
' '           Text
'c₂'          Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
')'           Operator
' '           Text
':='          Operator
' '           Text
'chain'       Name
' '           Text
'c₂'          Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
' '           Text
'⊂'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
'\n\n'        Text

'def'         Keyword.Declaration
' '           Text
'is_max_chain' Name
' '           Text
'('           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
')'           Operator
' '           Text
':='          Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'¬'           Name.Builtin.Pseudo
' '           Text
'('           Operator
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
')'           Operator
'\n\n'        Text

'def'         Keyword.Declaration
' '           Text
'succ_chain'  Name
' '           Text
'('           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'if'          Keyword
' '           Text
'h'           Name
' '           Text
':'           Operator
' '           Text
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
' '           Text
'then'        Keyword
' '           Text
'some'        Name
' '           Text
'h'           Name
' '           Text
'else'        Keyword
' '           Text
'c'           Name
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'succ_spec'   Name
' '           Text
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
' '           Text
'('           Operator
'h'           Name
' '           Text
':'           Operator
' '           Text
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'let'         Keyword
' '           Text
'⟨'           Operator
"c'"          Name
','           Operator
' '           Text
"hc'"         Name
'⟩'           Operator
' '           Text
':='          Operator
' '           Text
'h'           Name
' '           Text
'in'          Keyword
'\n'          Text

'have'        Keyword
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'some'        Name
' '           Text
'h'           Name
')'           Operator
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'@'           Name.Builtin.Pseudo
'some_spec'   Name
' '           Text
'_'           Name
' '           Text
'('           Operator
'λ'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
')'           Operator
' '           Text
'_'           Name
','           Operator
'\n'          Text

'by'          Keyword.Declaration
' '           Text
'simp'        Name
' '           Text
'['           Operator
'succ_chain'  Name
','           Operator
' '           Text
'dif_pos'     Name
','           Operator
' '           Text
'h'           Name
','           Operator
' '           Text
'this.right'  Name
']'           Operator
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_succ'  Name
' '           Text
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
' '           Text
'('           Operator
'hc'          Name
' '           Text
':'           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':'           Operator
' '           Text
'chain'       Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'if'          Keyword
' '           Text
'h'           Name
' '           Text
':'           Operator
' '           Text
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
' '           Text
'then'        Keyword
'\n  '        Text
'('           Operator
'succ_spec'   Name
' '           Text
'h'           Name
')'           Operator
'.'           Name.Builtin.Pseudo
'left'        Name
'\n'          Text

'else'        Keyword
'\n  '        Text
'by'          Keyword.Declaration
' '           Text
'simp'        Name
' '           Text
'['           Operator
'succ_chain'  Name
','           Operator
' '           Text
'dif_neg'     Name
','           Operator
' '           Text
'h'           Name
']'           Operator
';'           Name.Builtin.Pseudo
' '           Text
'exact'       Name
' '           Text
'hc'          Name
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'super_of_not_max' Name
' '           Text
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
')'           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'¬'           Name.Builtin.Pseudo
' '           Text
'is_max_chain' Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'begin'       Keyword.Declaration
'\n  '        Text
'simp'        Name
' '           Text
'['           Operator
'is_max_chain' Name
','           Operator
' '           Text
'not_and_iff' Name
','           Operator
' '           Text
'not_not_iff' Name
']'           Operator
' '           Text
'at'          Name
' '           Text
'hc₂'         Name
','           Operator
'\n  '        Text
'exact'       Name
' '           Text
'have'        Keyword
' '           Text
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
','           Operator
' '           Text
'from'        Keyword
' '           Text
'hc₂.neg_resolve_left' Name
' '           Text
'hc₁'         Name
','           Operator
'\n  '        Text
'let'         Keyword
' '           Text
'⟨'           Operator
"c'"          Name
','           Operator
' '           Text
"hc'"         Name
'⟩'           Operator
' '           Text
':='          Operator
' '           Text
'this'        Name
' '           Text
'in'          Keyword
'\n  '        Text
'show'        Keyword
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'c'           Name
')'           Operator
','           Operator
'\n    '      Text
'from'        Keyword
' '           Text
'succ_spec'   Name
' '           Text
'⟨'           Operator
"c'"          Name
','           Operator
' '           Text
'hc₁'         Name
','           Operator
' '           Text
"hc'"         Name
'⟩'           Operator
'\n'          Text

'end'         Keyword.Declaration
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'succ_increasing' Name
' '           Text
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
' '           Text
':'           Operator
' '           Text
'c'           Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'c'           Name
' '           Text
':='          Operator
'\n'          Text

'if'          Keyword
' '           Text
'h'           Name
' '           Text
':'           Operator
' '           Text
'∃'           Name.Builtin.Pseudo
"c'"          Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'∧'           Name.Builtin.Pseudo
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
"c'"          Name
' '           Text
'then'        Keyword
'\n  '        Text
'have'        Keyword
' '           Text
'super_chain' Name
' '           Text
'c'           Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'c'           Name
')'           Operator
','           Operator
' '           Text
'from'        Keyword
' '           Text
'succ_spec'   Name
' '           Text
'h'           Name
','           Operator
'\n  '        Text
'this.right.left' Name
'\n'          Text

'else'        Keyword
' '           Text
'by'          Keyword.Declaration
' '           Text
'simp'        Name
' '           Text
'['           Operator
'succ_chain'  Name
','           Operator
' '           Text
'dif_neg'     Name
','           Operator
' '           Text
'h'           Name
','           Operator
' '           Text
'subset.refl' Name
']'           Operator
'\n\n'        Text

'inductive'   Keyword.Declaration
' '           Text
'chain_closure' Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'Prop'        Keyword.Type
'\n'          Text

'|'           Name.Builtin.Pseudo
' '           Text
'succ'        Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'{'           Operator
's'           Name
'}'           Operator
','           Operator
' '           Text
'chain_closure' Name
' '           Text
's'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
's'           Name
')'           Operator
'\n'          Text

'|'           Name.Builtin.Pseudo
' '           Text
'union'       Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'{'           Operator
's'           Name
'}'           Operator
','           Operator
' '           Text
'('           Operator
'∀'           Name.Builtin.Pseudo
'a'           Name
'∈'           Name.Builtin.Pseudo
's'           Name
','           Operator
' '           Text
'chain_closure' Name
' '           Text
'a'           Name
')'           Operator
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
's'           Name
')'           Operator
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_closure_empty' Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'∅'           Name.Builtin.Pseudo
' '           Text
':='          Operator
'\n'          Text

'have'        Keyword
' '           Text
'chain_closure' Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'∅'           Name.Builtin.Pseudo
')'           Operator
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'chain_closure.union' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'a'           Name
' '           Text
'h'           Name
','           Operator
' '           Text
'h.rec'       Name
' '           Text
'_'           Name
','           Operator
'\n'          Text

'by'          Keyword.Declaration
' '           Text
'simp'        Name
' '           Text
'at'          Name
' '           Text
'this'        Name
';'           Name.Builtin.Pseudo
' '           Text
'assumption'  Name
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_closure_closure' Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
' '           Text
':='          Operator
'\n'          Text

'chain_closure.union' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
's'           Name
' '           Text
'hs'          Name
','           Operator
' '           Text
'hs'          Name
'\n\n'        Text

'variables'   Keyword.Declaration
' '           Text
'{'           Operator
'c'           Name
' '           Text
'c₁'          Name
' '           Text
'c₂'          Name
' '           Text
'c₃'          Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
'}'           Operator
'\n\n'        Text

'private'     Keyword.Namespace
' '           Text
'lemma'       Keyword.Declaration
' '           Text
'chain_closure_succ_total_aux' Name
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₁'          Name
')'           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₂'          Name
')'           Operator
'\n  '        Text
'('           Operator
'h'           Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'{'           Operator
'c₃'          Name
'}'           Operator
','           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₃'          Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'c₃'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'c₃'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'c₃'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'c₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
' '           Text
':='          Operator
'\n'          Text

'begin'       Keyword.Declaration
'\n  '        Text
'induction'   Name
' '           Text
'hc₁'         Name
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.succ' Name
' '           Text
'c₃'          Name
' '           Text
'hc₃'         Name
' '           Text
'ih'          Name
' '           Text
'{'           Operator
'\n    '      Text
'cases'       Name
' '           Text
'ih'          Name
' '           Text
'with'        Keyword
' '           Text
'ih'          Name
' '           Text
'ih'          Name
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'have'        Keyword
' '           Text
'h'           Name
' '           Text
':='          Operator
' '           Text
'h'           Name
' '           Text
'hc₃'         Name
' '           Text
'ih'          Name
','           Operator
'\n      '    Text
'cases'       Name
' '           Text
'h'           Name
' '           Text
'with'        Keyword
' '           Text
'h'           Name
' '           Text
'h'           Name
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'or.inr'      Name
' '           Text
'('           Operator
'h'           Name
' '           Text
'▸'           Name.Builtin.Pseudo
' '           Text
'subset.refl' Name
' '           Text
'_'           Name
')'           Operator
' '           Text
'}'           Operator
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'or.inl'      Name
' '           Text
'h'           Name
' '           Text
'}'           Operator
' '           Text
'}'           Operator
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'or.inr'      Name
' '           Text
'('           Operator
'subset.trans' Name
' '           Text
'ih'          Name
' '           Text
'succ_increasing' Name
')'           Operator
' '           Text
'}'           Operator
' '           Text
'}'           Operator
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.union' Name
' '           Text
's'           Name
' '           Text
'hs'          Name
' '           Text
'ih'          Name
' '           Text
'{'           Operator
'\n    '      Text
'refine'      Name
' '           Text
'('           Operator
"or_of_not_implies'" Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'λ'           Name.Builtin.Pseudo
' '           Text
'hn'          Name
','           Operator
' '           Text
'sUnion_subset' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'λ'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'ha'          Name
','           Operator
' '           Text
'_'           Name
')'           Operator
','           Operator
'\n    '      Text
'apply'       Name
' '           Text
'('           Operator
'ih'          Name
' '           Text
'a'           Name
' '           Text
'ha'          Name
')'           Operator
'.'           Name.Builtin.Pseudo
'resolve_right' Name
','           Operator
'\n    '      Text
'apply'       Name
' '           Text
'mt'          Name
' '           Text
'('           Operator
'λ'           Name.Builtin.Pseudo
' '           Text
'h'           Name
','           Operator
' '           Text
'_'           Name
')'           Operator
' '           Text
'hn'          Name
','           Operator
'\n    '      Text
'exact'       Name
' '           Text
'subset.trans' Name
' '           Text
'h'           Name
' '           Text
'('           Operator
'subset_sUnion_of_mem' Name
' '           Text
'ha'          Name
')'           Operator
' '           Text
'}'           Operator
'\n'          Text

'end'         Keyword.Declaration
'\n\n'        Text

'private'     Keyword.Namespace
' '           Text
'lemma'       Keyword.Declaration
' '           Text
'chain_closure_succ_total' Name
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₁'          Name
')'           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₂'          Name
')'           Operator
' '           Text
'('           Operator
'h'           Name
' '           Text
':'           Operator
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'c₂'          Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
':='          Operator
'\n'          Text

'begin'       Keyword.Declaration
'\n  '        Text
'induction'   Name
' '           Text
'hc₂'         Name
' '           Text
'generalizing' Name
' '           Text
'c₁'          Name
' '           Text
'hc₁'         Name
' '           Text
'h'           Name
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.succ' Name
' '           Text
'c₂'          Name
' '           Text
'hc₂'         Name
' '           Text
'ih'          Name
' '           Text
'{'           Operator
'\n    '      Text
'have'        Keyword
' '           Text
'h₁'          Name
' '           Text
':'           Operator
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'@'           Name.Builtin.Pseudo
'succ_chain'  Name
' '           Text
'α'           Name
' '           Text
'r'           Name
' '           Text
'c₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
' '           Text
':='          Operator
'\n      '    Text
'('           Operator
'chain_closure_succ_total_aux' Name
' '           Text
'hc₁'         Name
' '           Text
'hc₂'         Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'c₁'          Name
','           Operator
' '           Text
'ih'          Name
')'           Operator
','           Operator
'\n    '      Text
'cases'       Name
' '           Text
'h₁'          Name
' '           Text
'with'        Keyword
' '           Text
'h₁'          Name
' '           Text
'h₁'          Name
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'have'        Keyword
' '           Text
'h₂'          Name
' '           Text
':='          Operator
' '           Text
'ih'          Name
' '           Text
'hc₁'         Name
' '           Text
'h₁'          Name
','           Operator
'\n      '    Text
'cases'       Name
' '           Text
'h₂'          Name
' '           Text
'with'        Keyword
' '           Text
'h₂'          Name
' '           Text
'h₂'          Name
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'or.inr'      Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'h₂'          Name
' '           Text
'▸'           Name.Builtin.Pseudo
' '           Text
'subset.refl' Name
' '           Text
'_'           Name
')'           Operator
' '           Text
'}'           Operator
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'or.inr'      Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'subset.trans' Name
' '           Text
'h₂'          Name
' '           Text
'succ_increasing' Name
')'           Operator
' '           Text
'}'           Operator
' '           Text
'}'           Operator
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'or.inl'      Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'subset.antisymm' Name
' '           Text
'h₁'          Name
' '           Text
'h'           Name
')'           Operator
' '           Text
'}'           Operator
' '           Text
'}'           Operator
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.union' Name
' '           Text
's'           Name
' '           Text
'hs'          Name
' '           Text
'ih'          Name
' '           Text
'{'           Operator
'\n    '      Text
'apply'       Name
' '           Text
'or.imp'      Name
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
"h'"          Name
','           Operator
' '           Text
'subset.antisymm' Name
' '           Text
"h'"          Name
' '           Text
'h'           Name
')'           Operator
' '           Text
'id'          Name
','           Operator
'\n    '      Text
'apply'       Name
' '           Text
'classical.by_contradiction' Name
','           Operator
'\n    '      Text
'simp'        Name
' '           Text
'['           Operator
'not_or_iff'  Name
','           Operator
' '           Text
'sUnion_subset_iff' Name
','           Operator
' '           Text
'classical.not_forall_iff' Name
','           Operator
' '           Text
'not_implies_iff' Name
']'           Operator
','           Operator
'\n    '      Text
'intro'       Name
' '           Text
'h'           Name
','           Operator
' '           Text
'cases'       Name
' '           Text
'h'           Name
' '           Text
'with'        Keyword
' '           Text
'h₁'          Name
' '           Text
'h₂'          Name
','           Operator
' '           Text
'cases'       Name
' '           Text
'h₂'          Name
' '           Text
'with'        Keyword
' '           Text
'c₃'          Name
' '           Text
'h₂'          Name
','           Operator
' '           Text
'cases'       Name
' '           Text
'h₂'          Name
' '           Text
'with'        Keyword
' '           Text
'h₂'          Name
' '           Text
'hc₃'         Name
','           Operator
'\n    '      Text
'have'        Keyword
' '           Text
'h'           Name
' '           Text
':='          Operator
' '           Text
'chain_closure_succ_total_aux' Name
' '           Text
'hc₁'         Name
' '           Text
'('           Operator
'hs'          Name
' '           Text
'c₃'          Name
' '           Text
'hc₃'         Name
')'           Operator
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
'c₄'          Name
','           Operator
' '           Text
'ih'          Name
' '           Text
'_'           Name
' '           Text
'hc₃'         Name
')'           Operator
','           Operator
'\n    '      Text
'cases'       Name
' '           Text
'h'           Name
' '           Text
'with'        Keyword
' '           Text
'h'           Name
' '           Text
'h'           Name
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'have'        Keyword
' '           Text
"h'"          Name
' '           Text
':='          Operator
' '           Text
'ih'          Name
' '           Text
'c₃'          Name
' '           Text
'hc₃'         Name
' '           Text
'hc₁'         Name
' '           Text
'h'           Name
','           Operator
'\n      '    Text
'cases'       Name
' '           Text
"h'"          Name
' '           Text
'with'        Keyword
' '           Text
"h'"          Name
' '           Text
"h'"          Name
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'h₂'          Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
"h'"          Name
' '           Text
'▸'           Name.Builtin.Pseudo
' '           Text
'subset.refl' Name
' '           Text
'_'           Name
')'           Operator
' '           Text
'}'           Operator
','           Operator
'\n      '    Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'h₁'          Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'subset.trans' Name
' '           Text
"h'"          Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'subset_sUnion_of_mem' Name
' '           Text
'hc₃'         Name
')'           Operator
' '           Text
'}'           Operator
' '           Text
'}'           Operator
','           Operator
'\n    '      Text
'{'           Operator
' '           Text
'exact'       Name
' '           Text
'('           Operator
'h₂'          Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'subset.trans' Name
' '           Text
'succ_increasing' Name
' '           Text
'h'           Name
')'           Operator
' '           Text
'}'           Operator
' '           Text
'}'           Operator
'\n'          Text

'end'         Keyword.Declaration
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_closure_total' Name
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₁'          Name
')'           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₂'          Name
')'           Operator
' '           Text
':'           Operator
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
' '           Text
':='          Operator
'\n'          Text

'have'        Keyword
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'c₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'chain_closure_succ_total_aux' Name
' '           Text
'hc₁'         Name
' '           Text
'hc₂'         Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'c₃'          Name
' '           Text
'hc₃'         Name
','           Operator
' '           Text
'chain_closure_succ_total' Name
' '           Text
'hc₃'         Name
' '           Text
'hc₂'         Name
','           Operator
'\n'          Text

'or.imp_right' Name
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
':'           Operator
' '           Text
'succ_chain'  Name
' '           Text
'c₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₁'          Name
','           Operator
' '           Text
'subset.trans' Name
' '           Text
'succ_increasing' Name
' '           Text
'this'        Name
')'           Operator
' '           Text
'this'        Name
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_closure_succ_fixpoint' Name
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₁'          Name
')'           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c₂'          Name
')'           Operator
'\n  '        Text
'('           Operator
'h_eq'        Name
' '           Text
':'           Operator
' '           Text
'succ_chain'  Name
' '           Text
'c₂'          Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
')'           Operator
' '           Text
':'           Operator
' '           Text
'c₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'c₂'          Name
' '           Text
':='          Operator
'\n'          Text

'begin'       Keyword.Declaration
'\n  '        Text
'induction'   Name
' '           Text
'hc₁'         Name
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.succ' Name
' '           Text
'c₁'          Name
' '           Text
'hc₁'         Name
' '           Text
'h'           Name
' '           Text
'{'           Operator
'\n    '      Text
'exact'       Name
' '           Text
'or.elim'     Name
' '           Text
'('           Operator
'chain_closure_succ_total' Name
' '           Text
'hc₁'         Name
' '           Text
'hc₂'         Name
' '           Text
'h'           Name
')'           Operator
'\n      '    Text
'('           Operator
'assume'      Keyword
' '           Text
'h'           Name
','           Operator
' '           Text
'h'           Name
' '           Text
'▸'           Name.Builtin.Pseudo
' '           Text
'h_eq.symm'   Name
' '           Text
'▸'           Name.Builtin.Pseudo
' '           Text
'subset.refl' Name
' '           Text
'c₂'          Name
')'           Operator
' '           Text
'id'          Name
' '           Text
'}'           Operator
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.union' Name
' '           Text
's'           Name
' '           Text
'hs'          Name
' '           Text
'ih'          Name
' '           Text
'{'           Operator
'\n    '      Text
'exact'       Name
' '           Text
'('           Operator
'sUnion_subset' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'c₁'          Name
' '           Text
'hc₁'         Name
','           Operator
' '           Text
'ih'          Name
' '           Text
'c₁'          Name
' '           Text
'hc₁'         Name
')'           Operator
' '           Text
'}'           Operator
'\n'          Text

'end'         Keyword.Declaration
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_closure_succ_fixpoint_iff' Name
' '           Text
'('           Operator
'hc'          Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'succ_chain'  Name
' '           Text
'c'           Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'c'           Name
' '           Text
'↔'           Name.Builtin.Pseudo
' '           Text
'c'           Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
' '           Text
':='          Operator
'\n'          Text

'⟨'           Operator
'assume'      Keyword
' '           Text
'h'           Name
','           Operator
' '           Text
'subset.antisymm' Name
'\n    '      Text
'('           Operator
'subset_sUnion_of_mem' Name
' '           Text
'hc'          Name
')'           Operator
'\n    '      Text
'('           Operator
'chain_closure_succ_fixpoint' Name
' '           Text
'chain_closure_closure' Name
' '           Text
'hc'          Name
' '           Text
'h'           Name
')'           Operator
','           Operator
'\n  '        Text
'assume'      Keyword
' '           Text
':'           Operator
' '           Text
'c'           Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
' '           Text
'|'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
' '           Text
'c'           Name
'}'           Operator
','           Operator
'\n  '        Text
'subset.antisymm' Name
'\n    '      Text
'('           Operator
'calc'        Keyword
' '           Text
'succ_chain'  Name
' '           Text
'c'           Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
'{'           Operator
'c'           Name
' '           Text
':'           Operator
' '           Text
'set'         Name
' '           Text
'α'           Name
' '           Text
'|'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
' '           Text
'c'           Name
'}'           Operator
' '           Text
':'           Operator
'\n        '  Text
'subset_sUnion_of_mem' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'chain_closure.succ' Name
' '           Text
'hc'          Name
'\n      '    Text
'.'           Name.Builtin.Pseudo
'.'           Name.Builtin.Pseudo
'.'           Name.Builtin.Pseudo
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'c'           Name
' '           Text
':'           Operator
' '           Text
'this.symm'   Name
')'           Operator
'\n    '      Text
'succ_increasing' Name
'⟩'           Operator
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'chain_chain_closure' Name
' '           Text
'('           Operator
'hc'          Name
' '           Text
':'           Operator
' '           Text
'chain_closure' Name
' '           Text
'c'           Name
')'           Operator
' '           Text
':'           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
':='          Operator
'\n'          Text

'begin'       Keyword.Declaration
'\n  '        Text
'induction'   Name
' '           Text
'hc'          Name
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.succ' Name
' '           Text
'c'           Name
' '           Text
'hc'          Name
' '           Text
'h'           Name
' '           Text
'{'           Operator
'\n    '      Text
'exact'       Name
' '           Text
'chain_succ'  Name
' '           Text
'h'           Name
' '           Text
'}'           Operator
','           Operator
'\n  '        Text
'case'        Name
' '           Text
'_root_.zorn.chain_closure.union' Name
' '           Text
's'           Name
' '           Text
'hs'          Name
' '           Text
'h'           Name
' '           Text
'{'           Operator
'\n    '      Text
'have'        Keyword
' '           Text
'h'           Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'c'           Name
'∈'           Name.Builtin.Pseudo
's'           Name
','           Operator
' '           Text
'zorn.chain'  Name
' '           Text
'c'           Name
' '           Text
':='          Operator
' '           Text
'h'           Name
','           Operator
'\n    '      Text
'exact'       Name
' '           Text
'assume'      Keyword
' '           Text
'c₁'          Name
' '           Text
'⟨'           Operator
't₁'          Name
','           Operator
' '           Text
'ht₁'         Name
','           Operator
' '           Text
'('           Operator
'hc₁'         Name
' '           Text
':'           Operator
' '           Text
'c₁'          Name
' '           Text
'∈'           Name.Builtin.Pseudo
' '           Text
't₁'          Name
')'           Operator
'⟩'           Operator
' '           Text
'c₂'          Name
' '           Text
'⟨'           Operator
't₂'          Name
','           Operator
' '           Text
'ht₂'         Name
','           Operator
' '           Text
'('           Operator
'hc₂'         Name
' '           Text
':'           Operator
' '           Text
'c₂'          Name
' '           Text
'∈'           Name.Builtin.Pseudo
' '           Text
't₂'          Name
')'           Operator
'⟩'           Operator
' '           Text
'hneq'        Name
','           Operator
'\n      '    Text
'have'        Keyword
' '           Text
't₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
't₂'          Name
' '           Text
'∨'           Name.Builtin.Pseudo
' '           Text
't₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
't₁'          Name
','           Operator
' '           Text
'from'        Keyword
' '           Text
'chain_closure_total' Name
' '           Text
'('           Operator
'hs'          Name
' '           Text
'_'           Name
' '           Text
'ht₁'         Name
')'           Operator
' '           Text
'('           Operator
'hs'          Name
' '           Text
'_'           Name
' '           Text
'ht₂'         Name
')'           Operator
','           Operator
'\n      '    Text
'or.elim'     Name
' '           Text
'this'        Name
'\n        '  Text
'('           Operator
'assume'      Keyword
' '           Text
':'           Operator
' '           Text
't₁'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
't₂'          Name
','           Operator
' '           Text
'h'           Name
' '           Text
't₂'          Name
' '           Text
'ht₂'         Name
' '           Text
'c₁'          Name
' '           Text
'('           Operator
'this'        Name
' '           Text
'hc₁'         Name
')'           Operator
' '           Text
'c₂'          Name
' '           Text
'hc₂'         Name
' '           Text
'hneq'        Name
')'           Operator
'\n        '  Text
'('           Operator
'assume'      Keyword
' '           Text
':'           Operator
' '           Text
't₂'          Name
' '           Text
'⊆'           Name.Builtin.Pseudo
' '           Text
't₁'          Name
','           Operator
' '           Text
'h'           Name
' '           Text
't₁'          Name
' '           Text
'ht₁'         Name
' '           Text
'c₁'          Name
' '           Text
'hc₁'         Name
' '           Text
'c₂'          Name
' '           Text
'('           Operator
'this'        Name
' '           Text
'hc₂'         Name
')'           Operator
' '           Text
'hneq'        Name
')'           Operator
' '           Text
'}'           Operator
'\n'          Text

'end'         Keyword.Declaration
'\n\n'        Text

'def'         Keyword.Declaration
' '           Text
'max_chain'   Name
' '           Text
':='          Operator
' '           Text
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
'\n\n'        Text

'/--'         Literal.String.Doc
' '           Literal.String.Doc
'H'           Literal.String.Doc
'a'           Literal.String.Doc
'u'           Literal.String.Doc
's'           Literal.String.Doc
'd'           Literal.String.Doc
'o'           Literal.String.Doc
'r'           Literal.String.Doc
'f'           Literal.String.Doc
'f'           Literal.String.Doc
"'"           Literal.String.Doc
's'           Literal.String.Doc
' '           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'x'           Literal.String.Doc
'i'           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'l'           Literal.String.Doc
'i'           Literal.String.Doc
't'           Literal.String.Doc
'y'           Literal.String.Doc
' '           Literal.String.Doc
'p'           Literal.String.Doc
'r'           Literal.String.Doc
'i'           Literal.String.Doc
'n'           Literal.String.Doc
'c'           Literal.String.Doc
'i'           Literal.String.Doc
'p'           Literal.String.Doc
'l'           Literal.String.Doc
'e'           Literal.String.Doc
'\n'          Literal.String.Doc

'\n'          Literal.String.Doc

'T'           Literal.String.Doc
'h'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
'e'           Literal.String.Doc
'x'           Literal.String.Doc
'i'           Literal.String.Doc
's'           Literal.String.Doc
't'           Literal.String.Doc
's'           Literal.String.Doc
' '           Literal.String.Doc
'a'           Literal.String.Doc
' '           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'x'           Literal.String.Doc
'i'           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'l'           Literal.String.Doc
' '           Literal.String.Doc
't'           Literal.String.Doc
'o'           Literal.String.Doc
't'           Literal.String.Doc
'a'           Literal.String.Doc
'l'           Literal.String.Doc
'l'           Literal.String.Doc
'y'           Literal.String.Doc
' '           Literal.String.Doc
'o'           Literal.String.Doc
'r'           Literal.String.Doc
'd'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
'd'           Literal.String.Doc
' '           Literal.String.Doc
's'           Literal.String.Doc
'u'           Literal.String.Doc
'b'           Literal.String.Doc
's'           Literal.String.Doc
'e'           Literal.String.Doc
't'           Literal.String.Doc
' '           Literal.String.Doc
'o'           Literal.String.Doc
'f'           Literal.String.Doc
' '           Literal.String.Doc
'`'           Literal.String.Doc
'α'           Literal.String.Doc
'`'           Literal.String.Doc
'.'           Literal.String.Doc
'\n'          Literal.String.Doc

'N'           Literal.String.Doc
'o'           Literal.String.Doc
't'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
't'           Literal.String.Doc
'h'           Literal.String.Doc
'a'           Literal.String.Doc
't'           Literal.String.Doc
' '           Literal.String.Doc
'w'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
'd'           Literal.String.Doc
'o'           Literal.String.Doc
' '           Literal.String.Doc
'n'           Literal.String.Doc
'o'           Literal.String.Doc
't'           Literal.String.Doc
' '           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
'q'           Literal.String.Doc
'u'           Literal.String.Doc
'i'           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
'`'           Literal.String.Doc
'α'           Literal.String.Doc
'`'           Literal.String.Doc
' '           Literal.String.Doc
't'           Literal.String.Doc
'o'           Literal.String.Doc
' '           Literal.String.Doc
'b'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
'p'           Literal.String.Doc
'a'           Literal.String.Doc
'r'           Literal.String.Doc
't'           Literal.String.Doc
'i'           Literal.String.Doc
'a'           Literal.String.Doc
'l'           Literal.String.Doc
'l'           Literal.String.Doc
'y'           Literal.String.Doc
' '           Literal.String.Doc
'o'           Literal.String.Doc
'r'           Literal.String.Doc
'd'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
'd'           Literal.String.Doc
' '           Literal.String.Doc
'b'           Literal.String.Doc
'y'           Literal.String.Doc
' '           Literal.String.Doc
'`'           Literal.String.Doc
'r'           Literal.String.Doc
'`'           Literal.String.Doc
'.'           Literal.String.Doc
' '           Literal.String.Doc
'-/'          Literal.String.Doc
'\n'          Text

'theorem'     Keyword.Declaration
' '           Text
'max_chain_spec' Name
' '           Text
':'           Operator
' '           Text
'is_max_chain' Name
' '           Text
'max_chain'   Name
' '           Text
':='          Operator
'\n'          Text

'classical.by_contradiction' Name
' '           Text
'$'           Name.Builtin.Pseudo
'\n'          Text

'assume'      Keyword
' '           Text
':'           Operator
' '           Text
'¬'           Name.Builtin.Pseudo
' '           Text
'is_max_chain' Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
','           Operator
'\n'          Text

'have'        Keyword
' '           Text
'super_chain' Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
' '           Text
'('           Operator
'succ_chain'  Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
')'           Operator
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'super_of_not_max' Name
' '           Text
'('           Operator
'chain_chain_closure' Name
' '           Text
'chain_closure_closure' Name
')'           Operator
' '           Text
'this'        Name
','           Operator
'\n'          Text

'let'         Keyword
' '           Text
'⟨'           Operator
'h₁'          Name
','           Operator
' '           Text
'h₂'          Name
','           Operator
' '           Text
'('           Operator
'h₃'          Name
' '           Text
':'           Operator
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
' '           Text
'≠'           Name.Builtin.Pseudo
' '           Text
'succ_chain'  Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
')'           Operator
'⟩'           Operator
' '           Text
':='          Operator
' '           Text
'this'        Name
' '           Text
'in'          Keyword
'\n'          Text

'have'        Keyword
' '           Text
'succ_chain'  Name
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'('           Operator
'⋃'           Name.Builtin.Pseudo
'₀'           Name.Builtin.Pseudo
' '           Text
'chain_closure' Name
')'           Operator
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'('           Operator
'chain_closure_succ_fixpoint_iff' Name
' '           Text
'chain_closure_closure' Name
')'           Operator
'.'           Name.Builtin.Pseudo
'mpr'         Name
' '           Text
'rfl'         Name
','           Operator
'\n'          Text

'h₃'          Name
' '           Text
'this.symm'   Name
'\n\n'        Text

'/--'         Literal.String.Doc
' '           Literal.String.Doc
'Z'           Literal.String.Doc
'o'           Literal.String.Doc
'r'           Literal.String.Doc
'n'           Literal.String.Doc
"'"           Literal.String.Doc
's'           Literal.String.Doc
' '           Literal.String.Doc
'l'           Literal.String.Doc
'e'           Literal.String.Doc
'm'           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'\n'          Literal.String.Doc

'\n'          Literal.String.Doc

'I'           Literal.String.Doc
'f'           Literal.String.Doc
' '           Literal.String.Doc
'e'           Literal.String.Doc
'v'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
'y'           Literal.String.Doc
' '           Literal.String.Doc
'c'           Literal.String.Doc
'h'           Literal.String.Doc
'a'           Literal.String.Doc
'i'           Literal.String.Doc
'n'           Literal.String.Doc
' '           Literal.String.Doc
'h'           Literal.String.Doc
'a'           Literal.String.Doc
's'           Literal.String.Doc
' '           Literal.String.Doc
'a'           Literal.String.Doc
'n'           Literal.String.Doc
' '           Literal.String.Doc
'u'           Literal.String.Doc
'p'           Literal.String.Doc
'p'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
' '           Literal.String.Doc
'b'           Literal.String.Doc
'o'           Literal.String.Doc
'u'           Literal.String.Doc
'n'           Literal.String.Doc
'd'           Literal.String.Doc
','           Literal.String.Doc
' '           Literal.String.Doc
't'           Literal.String.Doc
'h'           Literal.String.Doc
'e'           Literal.String.Doc
'n'           Literal.String.Doc
' '           Literal.String.Doc
't'           Literal.String.Doc
'h'           Literal.String.Doc
'e'           Literal.String.Doc
'r'           Literal.String.Doc
'e'           Literal.String.Doc
' '           Literal.String.Doc
'i'           Literal.String.Doc
's'           Literal.String.Doc
' '           Literal.String.Doc
'a'           Literal.String.Doc
' '           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'x'           Literal.String.Doc
'i'           Literal.String.Doc
'm'           Literal.String.Doc
'a'           Literal.String.Doc
'l'           Literal.String.Doc
' '           Literal.String.Doc
'e'           Literal.String.Doc
'l'           Literal.String.Doc
'e'           Literal.String.Doc
'm'           Literal.String.Doc
'e'           Literal.String.Doc
'n'           Literal.String.Doc
't'           Literal.String.Doc
' '           Literal.String.Doc
'-/'          Literal.String.Doc
'\n'          Text

'theorem'     Keyword.Declaration
' '           Text
'zorn'        Name
' '           Text
'('           Operator
'h'           Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'c'           Name
','           Operator
' '           Text
'chain'       Name
' '           Text
'c'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'∃'           Name.Builtin.Pseudo
'ub'          Name
','           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
'∈'           Name.Builtin.Pseudo
'c'           Name
','           Operator
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'ub'          Name
')'           Operator
' '           Text
'('           Operator
'trans'       Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'{'           Operator
'a'           Name
' '           Text
'b'           Name
' '           Text
'c'           Name
'}'           Operator
','           Operator
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'b'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'b'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'c'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'c'           Name
')'           Operator
' '           Text
':'           Operator
'\n  '        Text
'∃'           Name.Builtin.Pseudo
'm'           Name
','           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
','           Operator
' '           Text
'm'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'm'           Name
' '           Text
':='          Operator
'\n'          Text

'have'        Keyword
' '           Text
'∃'           Name.Builtin.Pseudo
'ub'          Name
','           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
'∈'           Name.Builtin.Pseudo
'max_chain'   Name
','           Operator
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'ub'          Name
','           Operator
'\n  '        Text
'from'        Keyword
' '           Text
'h'           Name
' '           Text
'_'           Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'max_chain_spec.left' Name
','           Operator
'\n'          Text

'let'         Keyword
' '           Text
'⟨'           Operator
'ub'          Name
','           Operator
' '           Text
'('           Operator
'hub'         Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
'∈'           Name.Builtin.Pseudo
'max_chain'   Name
','           Operator
' '           Text
'a'           Name
' '           Text
'≺'           Name.Builtin.Pseudo
' '           Text
'ub'          Name
')'           Operator
'⟩'           Operator
' '           Text
':='          Operator
' '           Text
'this'        Name
' '           Text
'in'          Keyword
'\n'          Text

'⟨'           Operator
'ub'          Name
','           Operator
' '           Text
'assume'      Keyword
' '           Text
'a'           Name
' '           Text
'ha'          Name
','           Operator
'\n  '        Text
'have'        Keyword
' '           Text
'chain'       Name
' '           Text
'('           Operator
'insert'      Name
' '           Text
'a'           Name
' '           Text
'max_chain'   Name
')'           Operator
','           Operator
'\n    '      Text
'from'        Keyword
' '           Text
'chain_insert' Name
' '           Text
'max_chain_spec.left' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'b'           Name
' '           Text
'hb'          Name
' '           Text
'_'           Name
','           Operator
' '           Text
'or.inr'      Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'trans'       Name
' '           Text
'('           Operator
'hub'         Name
' '           Text
'b'           Name
' '           Text
'hb'          Name
')'           Operator
' '           Text
'ha'          Name
','           Operator
'\n  '        Text
'have'        Keyword
' '           Text
'a'           Name
' '           Text
'∈'           Name.Builtin.Pseudo
' '           Text
'max_chain'   Name
','           Operator
' '           Text
'from'        Keyword
'\n    '      Text
'classical.by_contradiction' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'assume'      Keyword
' '           Text
'h'           Name
' '           Text
':'           Operator
' '           Text
'a'           Name
' '           Text
'∉'           Name.Builtin.Pseudo
' '           Text
'max_chain'   Name
','           Operator
'\n    '      Text
'max_chain_spec.right' Name
' '           Text
'$'           Name.Builtin.Pseudo
' '           Text
'⟨'           Operator
'insert'      Name
' '           Text
'a'           Name
' '           Text
'max_chain'   Name
','           Operator
' '           Text
'this'        Name
','           Operator
' '           Text
'ssubset_insert' Name
' '           Text
'h'           Name
'⟩'           Operator
','           Operator
'\n  '        Text
'hub'         Name
' '           Text
'a'           Name
' '           Text
'this'        Name
'⟩'           Operator
'\n\n'        Text

'end'         Keyword.Declaration
' '           Text
'chain'       Name
'\n\n'        Text

'theorem'     Keyword.Declaration
' '           Text
'zorn_weak_order' Name
' '           Text
'{'           Operator
'α'           Name
' '           Text
':'           Operator
' '           Text
'Type'        Keyword.Type
' '           Text
'u'           Name
'}'           Operator
' '           Text
'['           Operator
'weak_order'  Name
' '           Text
'α'           Name
']'           Operator
'\n  '        Text
'('           Operator
'h'           Name
' '           Text
':'           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'c'           Name
':'           Operator
'set'         Name
' '           Text
'α'           Name
','           Operator
' '           Text
'@'           Name.Builtin.Pseudo
'chain'       Name
' '           Text
'α'           Name
' '           Text
'('           Operator
'≤'           Name.Builtin.Pseudo
')'           Operator
' '           Text
'c'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'∃'           Name.Builtin.Pseudo
'ub'          Name
','           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
'∈'           Name.Builtin.Pseudo
'c'           Name
','           Operator
' '           Text
'a'           Name
' '           Text
'≤'           Name.Builtin.Pseudo
' '           Text
'ub'          Name
')'           Operator
' '           Text
':'           Operator
' '           Text
'∃'           Name.Builtin.Pseudo
'm'           Name
':'           Operator
'α'           Name
','           Operator
' '           Text
'∀'           Name.Builtin.Pseudo
'a'           Name
','           Operator
' '           Text
'm'           Name
' '           Text
'≤'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'→'           Name.Builtin.Pseudo
' '           Text
'a'           Name
' '           Text
'='           Name.Builtin.Pseudo
' '           Text
'm'           Name
' '           Text
':='          Operator
'\n'          Text

'let'         Keyword
' '           Text
'⟨'           Operator
'm'           Name
','           Operator
' '           Text
'hm'          Name
'⟩'           Operator
' '           Text
':='          Operator
' '           Text
'@'           Name.Builtin.Pseudo
'zorn'        Name
' '           Text
'α'           Name
' '           Text
'('           Operator
'≤'           Name.Builtin.Pseudo
')'           Operator
' '           Text
'h'           Name
' '           Text
'('           Operator
'assume'      Keyword
' '           Text
'a'           Name
' '           Text
'b'           Name
' '           Text
'c'           Name
','           Operator
' '           Text
'le_trans'    Name
')'           Operator
' '           Text
'in'          Keyword
'\n'          Text

'⟨'           Operator
'm'           Name
','           Operator
' '           Text
'assume'      Keyword
' '           Text
'a'           Name
' '           Text
'ha'          Name
','           Operator
' '           Text
'le_antisymm' Name
' '           Text
'('           Operator
'hm'          Name
' '           Text
'a'           Name
' '           Text
'ha'          Name
')'           Operator
' '           Text
'ha'          Name
'⟩'           Operator
'\n\n'        Text

'end'         Keyword.Declaration
' '           Text
'zorn'        Name
'\n'          Text
