'/-'          Comment
"\nCopyright (c) 2017 Johannes Hölzl. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Johannes Hölzl\n\nZorn's lemmas.\n\nPorted from Isabelle" Comment.Multiline
'/'           Comment.Multiline
'HOL (written by Jacques D. Fleuriot, Tobias Nipkow, and Christian Sternagel).\n' Comment.Multiline

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

'/--'         Literal.String.Doc
" Hausdorff's maximality principle\n\nThere exists a maximal totally ordered subset of `α`.\nNote that we do not require `α` to be partially ordered by `r`. " Literal.String.Doc
'-/'          Literal.String.Doc
'\n'          Text.Whitespace

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

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

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

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

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

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

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

'/--'         Literal.String.Doc
" Zorn's lemma\n\nIf every chain has an upper bound, then there is a maximal element " Literal.String.Doc
'-/'          Literal.String.Doc
'\n'          Text.Whitespace

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

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

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

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

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

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

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

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

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

'-- other bits of tricky syntax' Comment.Single
'\n'          Text.Whitespace

'@['          Keyword.Declaration
'to_additive' Name
' '           Text.Whitespace
'"'           Literal.String.Double
'See note [foo]' Literal.String.Double
'"'           Literal.String.Double
']'           Keyword.Declaration
'\n'          Text.Whitespace

'lemma'       Keyword.Declaration
' '           Text.Whitespace
'mul_one'     Name
' '           Text.Whitespace
':'           Operator
' '           Text.Whitespace
'sorry'       Generic.Error
' '           Text.Whitespace
':='          Operator
' '           Text.Whitespace
'sorry'       Generic.Error
'\n\n'        Text.Whitespace

'variables'   Keyword.Declaration
' '           Text.Whitespace
'{'           Operator
'ι'           Name
' '           Text.Whitespace
'A'           Name
' '           Text.Whitespace
'B'           Name
' '           Text.Whitespace
':'           Operator
' '           Text.Whitespace
'Type'        Keyword.Type
'*'           Name.Builtin.Pseudo
'}'           Operator
' '           Text.Whitespace
'('           Operator
'𝒜'           Name
' '           Text.Whitespace
':'           Operator
' '           Text.Whitespace
'ι'           Name
' '           Text.Whitespace
'→'           Name.Builtin.Pseudo
' '           Text.Whitespace
'A'           Name
')'           Operator
' '           Text.Whitespace
'('           Operator
'ℬ'           Name
' '           Text.Whitespace
':'           Operator
' '           Text.Whitespace
'ι'           Name
' '           Text.Whitespace
'→'           Name.Builtin.Pseudo
' '           Text.Whitespace
'B'           Name
')'           Operator
'\n\n'        Text.Whitespace

'#check'      Keyword
' '           Text.Whitespace
'`𝒜.a'        Literal.String.Symbol
'\n'          Text.Whitespace

'#check'      Keyword
' '           Text.Whitespace
'``𝒜'         Literal.String.Symbol
'\n'          Text.Whitespace
