coffee/coffee.pygments
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
This repository has been archived on 2024-06-20. You can view files and clone it, but you cannot make any changes to it's state, such as pushing and creating new issues, pull requests or comments.
coffee.pygments/tests/examplefiles/lean/test.lean.output

3632 lines
80 KiB
Text
Generated
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

'/-' 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\n' Text
'-- other bits of tricky syntax' Comment.Single
'\n' Text
'@[' Keyword.Declaration
'to_additive' Name
' ' Text
'"' Literal.String.Double
'See note [foo]' Literal.String.Double
'"' Literal.String.Double
']' Keyword.Declaration
'\n' Text
'lemma' Keyword.Declaration
' ' Text
'mul_one' Name
' ' Text
':' Operator
' ' Text
'sorry' Generic.Error
' ' Text
':=' Operator
' ' Text
'sorry' Generic.Error
'\n' Text
Reference in a new issue View git blame Copy permalink