diff options
Diffstat (limited to 'tests/lexers/lean')
| -rw-r--r-- | tests/lexers/lean/example.txt | 3819 |
1 files changed, 3819 insertions, 0 deletions
diff --git a/tests/lexers/lean/example.txt b/tests/lexers/lean/example.txt new file mode 100644 index 00000000..8f003e7c --- /dev/null +++ b/tests/lexers/lean/example.txt @@ -0,0 +1,3819 @@ +---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 |