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