Skip to content

Instantly share code, notes, and snippets.

@fpvandoorn

fpvandoorn/MessyCode.lean

Last active October 9, 2023 17:45
Show Gist options
  • Save fpvandoorn/c398ea0a926a8b4013344d4a45bf9bbb to your computer and use it in GitHub Desktop.
Save fpvandoorn/c398ea0a926a8b4013344d4a45bf9bbb to your computer and use it in GitHub Desktop.
Download ZIP
Some experiments using type class graphs in Lean 4
Raw
full.dot
digraph "instance_graph" {
"ConditionallyCompleteLinearOrderedField" -> "InfSet";
"ConditionallyCompleteLinearOrderedField" -> "SupSet";
"ConditionallyCompleteLinearOrderedField" -> "Sup";
"ConditionallyCompleteLinearOrderedField" -> "ConditionallyCompleteLinearOrder";
"ConditionallyCompleteLinearOrderedField" -> "Inf";
"ConditionallyCompleteLinearOrderedField" -> "LinearOrderedField";
"ConditionallyCompleteLinearOrderedField" -> "Archimedean";
"BiheytingAlgebra" -> "CoheytingAlgebra";
"BiheytingAlgebra" -> "HNot";
"BiheytingAlgebra" -> "SDiff";
"BiheytingAlgebra" -> "HeytingAlgebra";
"UpgradedPolishSpace" -> "CompleteSpace";
"UpgradedPolishSpace" -> "MetricSpace";
"UpgradedPolishSpace" -> "TopologicalSpace.SecondCountableTopology";
"Nontrivial" -> "Nonempty";
"SeparatedSpace" -> "T3Space";
"Semigroup" -> "Dvd";
"Semigroup" -> "Mul";
"Semigroup" -> "IsJordan";
"CanonicallyLinearOrderedSemifield" -> "Nontrivial";
"CanonicallyLinearOrderedSemifield" -> "Inv";
"CanonicallyLinearOrderedSemifield" -> "Ord";
"CanonicallyLinearOrderedSemifield" -> "Max";
"CanonicallyLinearOrderedSemifield" -> "Div";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedCommGroupWithZero";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedSemifield";
"CanonicallyLinearOrderedSemifield" -> "Min";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyLinearOrderedAddMonoid";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyOrderedCommSemiring";
"StrictOrderedCommRing" -> "CommRing";
"StrictOrderedCommRing" -> "OrderedCommRing";
"StrictOrderedCommRing" -> "StrictOrderedRing";
"StrictOrderedCommRing" -> "StrictOrderedCommSemiring";
"TopologicalSpace.PseudoMetrizableSpace" -> "TopologicalSpace.FirstCountableTopology";
"OrderedCommGroup" -> "PartialOrder";
"OrderedCommGroup" -> "CommGroup";
"OrderedCommGroup" -> "OrderedCancelCommMonoid";
"Monoid" -> "Semigroup";
"Monoid" -> "One";
"Monoid" -> "MulOneClass";
"UniformSpace" -> "RegularSpace";
"UniformSpace" -> "TopologicalSpace";
"NonUnitalNonAssocRing" -> "Mul";
"NonUnitalNonAssocRing" -> "AddCommGroup";
"NonUnitalNonAssocRing" -> "HasDistribNeg";
"NonUnitalNonAssocRing" -> "NonUnitalNonAssocSemiring";
"LinearOrderedCancelAddCommMonoid" -> "Ord";
"LinearOrderedCancelAddCommMonoid" -> "Max";
"LinearOrderedCancelAddCommMonoid" -> "LinearOrderedAddCommMonoid";
"LinearOrderedCancelAddCommMonoid" -> "Min";
"LinearOrderedCancelAddCommMonoid" -> "OrderedCancelAddCommMonoid";
"SemigroupWithZero" -> "Semigroup";
"SemigroupWithZero" -> "MulZeroClass";
"SemigroupWithZero" -> "Zero";
"CategoryTheory.RegularMonoCategory" -> "CategoryTheory.StrongMonoCategory";
"Lattice" -> "SemilatticeInf";
"Lattice" -> "SemilatticeSup";
"Lattice" -> "Inf";
"BooleanAlgebra" -> "BiheytingAlgebra";
"BooleanAlgebra" -> "HImp";
"BooleanAlgebra" -> "HasCompl";
"BooleanAlgebra" -> "Bot";
"BooleanAlgebra" -> "DistribLattice";
"BooleanAlgebra" -> "ComplementedLattice";
"BooleanAlgebra" -> "GeneralizedBooleanAlgebra";
"BooleanAlgebra" -> "SDiff";
"BooleanAlgebra" -> "BoundedOrder";
"BooleanAlgebra" -> "Top";
"MeasurableInf₂" -> "MeasurableInf";
"OrderedCommMonoid" -> "PartialOrder";
"OrderedCommMonoid" -> "CommMonoid";
"NonarchimedeanAddGroup" -> "TopologicalAddGroup";
"CategoryTheory.Limits.HasZeroMorphisms" -> "CategoryTheory.Limits.MonoCoprod";
"IsDomain" -> "Nontrivial";
"IsDomain" -> "IsCancelMulZero";
"IsDomain" -> "CancelMonoidWithZero";
"NonUnitalSeminormedRing" -> "SeminormedAddCommGroup";
"NonUnitalSeminormedRing" -> "Norm";
"NonUnitalSeminormedRing" -> "ContinuousMul";
"NonUnitalSeminormedRing" -> "PseudoMetricSpace";
"NonUnitalSeminormedRing" -> "NonUnitalRing";
"NonUnitalSeminormedRing" -> "TopologicalRing";
"OrderedAddCommMonoid" -> "PartialOrder";
"OrderedAddCommMonoid" -> "AddCommMonoid";
"CompleteSemilatticeSup" -> "PartialOrder";
"CompleteSemilatticeSup" -> "SupSet";
"CommRing" -> "AddCommGroupWithOne";
"CommRing" -> "NonUnitalCommRing";
"CommRing" -> "CommSemiring";
"CommRing" -> "CommMonoid";
"CommRing" -> "Ring";
"LipschitzAdd" -> "ContinuousAdd";
"LinearOrderedAddCommGroupWithTop" -> "Nontrivial";
"LinearOrderedAddCommGroupWithTop" -> "SubNegMonoid";
"LinearOrderedAddCommGroupWithTop" -> "Neg";
"LinearOrderedAddCommGroupWithTop" -> "LinearOrderedAddCommMonoidWithTop";
"LinearOrderedAddCommGroupWithTop" -> "Sub";
"StrictOrderedSemiring" -> "Nontrivial";
"StrictOrderedSemiring" -> "NoMaxOrder";
"StrictOrderedSemiring" -> "PartialOrder";
"StrictOrderedSemiring" -> "OrderedSemiring";
"StrictOrderedSemiring" -> "CharZero";
"StrictOrderedSemiring" -> "OrderedCancelAddCommMonoid";
"StrictOrderedSemiring" -> "Semiring";
"TopologicalDivisionRing" -> "HasContinuousInv₀";
"TopologicalDivisionRing" -> "TopologicalRing";
"CategoryTheory.Noetherian" -> "CategoryTheory.EssentiallySmall";
"AddCommGroupWithOne" -> "One";
"AddCommGroupWithOne" -> "IntCast";
"AddCommGroupWithOne" -> "AddCommMonoidWithOne";
"AddCommGroupWithOne" -> "AddCommGroup";
"AddCommGroupWithOne" -> "NatCast";
"AddCommGroupWithOne" -> "AddGroupWithOne";
"One" -> "Nonempty";
"SeminormedAddCommGroup" -> "LipschitzAdd";
"SeminormedAddCommGroup" -> "SeminormedAddGroup";
"SeminormedAddCommGroup" -> "AddCommGroup";
"SeminormedAddCommGroup" -> "Norm";
"SeminormedAddCommGroup" -> "PseudoMetricSpace";
"SeminormedAddCommGroup" -> "TopologicalAddGroup";
"SeminormedAddCommGroup" -> "UniformAddGroup";
"TopologicalSpace.MetrizableSpace" -> "TopologicalSpace.PseudoMetrizableSpace";
"TopologicalSpace.MetrizableSpace" -> "T2Space";
"AddLeftCancelSemigroup" -> "AddSemigroup";
"AddLeftCancelSemigroup" -> "IsLeftCancelAdd";
"LinearOrderedCommGroup" -> "OrderedCommGroup";
"LinearOrderedCommGroup" -> "Ord";
"LinearOrderedCommGroup" -> "LinearOrder";
"LinearOrderedCommGroup" -> "Max";
"LinearOrderedCommGroup" -> "LinearOrderedCancelCommMonoid";
"LinearOrderedCommGroup" -> "Min";
"AddCancelCommMonoid" -> "AddLeftCancelMonoid";
"AddCancelCommMonoid" -> "AddCancelMonoid";
"AddCancelCommMonoid" -> "AddCommMonoid";
"CategoryTheory.RegularEpiCategory" -> "CategoryTheory.StrongEpiCategory";
"NormedCommRing" -> "SeminormedCommRing";
"NormedCommRing" -> "NormedRing";
"SeminormedCommRing" -> "CommRing";
"SeminormedCommRing" -> "SeminormedRing";
"TopologicalGroup" -> "RegularSpace";
"TopologicalGroup" -> "HSpace";
"TopologicalGroup" -> "ContinuousMul";
"TopologicalGroup" -> "ContinuousInv";
"TopologicalGroup" -> "ContinuousDiv";
"KleeneAlgebra" -> "KStar";
"KleeneAlgebra" -> "IdemSemiring";
"Quandle" -> "Rack";
"TopologicalSpace.FirstCountableTopology" -> "FrechetUrysohnSpace";
"OrderedRing" -> "PartialOrder";
"OrderedRing" -> "OrderedSemiring";
"OrderedRing" -> "OrderedAddCommGroup";
"OrderedRing" -> "Ring";
"CategoryTheory.IsCofiltered" -> "CategoryTheory.IsCofilteredOrEmpty";
"IsLowerModularLattice" -> "IsWeakLowerModularLattice";
"CategoryTheory.FinitaryExtensive" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.FinitaryExtensive" -> "CategoryTheory.Limits.HasStrictInitialObjects";
"LinearOrderedCommSemiring" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedCommSemiring" -> "Ord";
"LinearOrderedCommSemiring" -> "Max";
"LinearOrderedCommSemiring" -> "Min";
"LinearOrderedCommSemiring" -> "StrictOrderedCommSemiring";
"LinearOrderedCommSemiring" -> "LinearOrderedSemiring";
"DiscreteTopology" -> "TopologicalSpace.MetrizableSpace";
"DiscreteTopology" -> "TopologicalSpace.FirstCountableTopology";
"DiscreteTopology" -> "T2Space";
"DiscreteTopology" -> "TotallySeparatedSpace";
"DiscreteTopology" -> "LocallyConnectedSpace";
"NormedGroup" -> "SeminormedGroup";
"NormedGroup" -> "Group";
"NormedGroup" -> "Norm";
"NormedGroup" -> "MetricSpace";
"LinearOrder" -> "Lattice";
"LinearOrder" -> "Ord";
"LinearOrder" -> "Max";
"LinearOrder" -> "PartialOrder";
"LinearOrder" -> "Min";
"LinearOrder" -> "DistribLattice";
"SeminormedGroup" -> "Group";
"SeminormedGroup" -> "NNNorm";
"SeminormedGroup" -> "Norm";
"SeminormedGroup" -> "PseudoMetricSpace";
"CategoryTheory.Limits.HasFiniteLimits" -> "CategoryTheory.Limits.HasFiniteProducts";
"Finite" -> "Countable";
"Unique" -> "Fintype";
"Unique" -> "Inhabited";
"Unique" -> "Subsingleton";
"ConditionallyCompleteLinearOrderBot" -> "OrderBot";
"ConditionallyCompleteLinearOrderBot" -> "Bot";
"ConditionallyCompleteLinearOrderBot" -> "ConditionallyCompleteLinearOrder";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasFiniteProducts";
"InvolutiveStar" -> "Star";
"NormalizedGCDMonoid" -> "GCDMonoid";
"NormalizedGCDMonoid" -> "NormalizationMonoid";
"CancelCommMonoidWithZero" -> "IsLeftCancelMulZero";
"CancelCommMonoidWithZero" -> "CommMonoidWithZero";
"CancelCommMonoidWithZero" -> "CancelMonoidWithZero";
"SeminormedAddGroup" -> "NNNorm";
"SeminormedAddGroup" -> "Norm";
"SeminormedAddGroup" -> "PseudoMetricSpace";
"SeminormedAddGroup" -> "AddGroup";
"DivisionCommMonoid" -> "DivisionMonoid";
"DivisionCommMonoid" -> "CommMonoid";
"GroupWithZero" -> "Nontrivial";
"GroupWithZero" -> "Inv";
"GroupWithZero" -> "DivisionMonoid";
"GroupWithZero" -> "Div";
"GroupWithZero" -> "DivInvMonoid";
"GroupWithZero" -> "MonoidWithZero";
"GroupWithZero" -> "NoZeroDivisors";
"GroupWithZero" -> "CancelMonoidWithZero";
"Rack" -> "Shelf";
"CompleteAtomicBooleanAlgebra" -> "HImp";
"CompleteAtomicBooleanAlgebra" -> "CompletelyDistribLattice";
"CompleteAtomicBooleanAlgebra" -> "CompleteBooleanAlgebra";
"CompleteAtomicBooleanAlgebra" -> "HasCompl";
"CompleteAtomicBooleanAlgebra" -> "IsCoatomistic";
"CompleteAtomicBooleanAlgebra" -> "SDiff";
"CompleteAtomicBooleanAlgebra" -> "IsAtomistic";
"IsSimpleOrder" -> "Nontrivial";
"NormedLatticeAddCommGroup" -> "Lattice";
"NormedLatticeAddCommGroup" -> "TopologicalLattice";
"NormedLatticeAddCommGroup" -> "ContinuousSup";
"NormedLatticeAddCommGroup" -> "OrderClosedTopology";
"NormedLatticeAddCommGroup" -> "ContinuousInf";
"NormedLatticeAddCommGroup" -> "HasSolidNorm";
"NormedLatticeAddCommGroup" -> "OrderedAddCommGroup";
"NormedLatticeAddCommGroup" -> "NormedAddCommGroup";
"ConditionallyCompleteLattice" -> "Lattice";
"ConditionallyCompleteLattice" -> "InfSet";
"ConditionallyCompleteLattice" -> "SupSet";
"IsCancelMul" -> "IsLeftCancelMul";
"IsCancelMul" -> "IsRightCancelMul";
"CategoryTheory.Limits.HasColimitsOfSize" -> "CategoryTheory.Limits.HasFiniteColimits";
"GeneralizedCoheytingAlgebra" -> "Lattice";
"GeneralizedCoheytingAlgebra" -> "OrderBot";
"GeneralizedCoheytingAlgebra" -> "Bot";
"GeneralizedCoheytingAlgebra" -> "DistribLattice";
"GeneralizedCoheytingAlgebra" -> "SDiff";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasZeroMorphisms";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasCokernels";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.NormalMonoCategory";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasKernels";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.NormalEpiCategory";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasFiniteProducts";
"WithIdeal" -> "UniformSpace";
"WithIdeal" -> "TopologicalSpace";
"WithIdeal" -> "NonarchimedeanRing";
"WithIdeal" -> "UniformAddGroup";
"Group" -> "DivisionMonoid";
"Group" -> "DivInvMonoid";
"Group" -> "CancelMonoid";
"CompleteDistribLattice" -> "Order.Coframe";
"CompleteDistribLattice" -> "Order.Frame";
"MeasurableSub₂" -> "MeasurableSub";
"SubNegMonoid" -> "Neg";
"SubNegMonoid" -> "AddMonoid";
"SubNegMonoid" -> "Sub";
"DivInvOneMonoid" -> "DivInvMonoid";
"DivInvOneMonoid" -> "InvOneClass";
"GroupFilterBasis" -> "TopologicalGroup";
"IsCommJordan" -> "IsJordan";
"CategoryTheory.Abelian" -> "CategoryTheory.IsIdempotentComplete";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteLimits";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasStrongEpiMonoFactorisations";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasCokernels";
"CategoryTheory.Abelian" -> "CategoryTheory.Preadditive";
"CategoryTheory.Abelian" -> "CategoryTheory.NormalMonoCategory";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasKernels";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasBinaryBiproducts";
"CategoryTheory.Abelian" -> "CategoryTheory.NormalEpiCategory";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteProducts";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteColimits";
"OrderBot" -> "Bot";
"AddLeftCancelMonoid" -> "AddLeftCancelSemigroup";
"AddLeftCancelMonoid" -> "AddMonoid";
"AddLeftCancelMonoid" -> "Zero";
"LipschitzMul" -> "ContinuousMul";
"AddCommMonoidWithOne" -> "AddCommMonoid";
"AddCommMonoidWithOne" -> "AddMonoidWithOne";
"MulZeroClass" -> "Mul";
"MulZeroClass" -> "Zero";
"RingFilterBasis" -> "AddGroupFilterBasis";
"RingFilterBasis" -> "TopologicalRing";
"IsUpperModularLattice" -> "IsWeakUpperModularLattice";
"LinearOrderedRing" -> "IsDomain";
"LinearOrderedRing" -> "Ord";
"LinearOrderedRing" -> "LinearOrder";
"LinearOrderedRing" -> "Max";
"LinearOrderedRing" -> "Min";
"LinearOrderedRing" -> "NoZeroDivisors";
"LinearOrderedRing" -> "LinearOrderedAddCommGroup";
"LinearOrderedRing" -> "StrictOrderedRing";
"LinearOrderedRing" -> "LinearOrderedSemiring";
"BorelSpace" -> "OpensMeasurableSpace";
"AddCancelMonoid" -> "AddLeftCancelMonoid";
"AddCancelMonoid" -> "AddRightCancelMonoid";
"AddCancelMonoid" -> "IsCancelAdd";
"UniformGroup" -> "TopologicalGroup";
"PartialOrder" -> "Preorder";
"CategoryTheory.Groupoid" -> "Quiver.HasInvolutiveReverse";
"CategoryTheory.Groupoid" -> "CategoryTheory.Category";
"AddCommGroup" -> "AddCancelCommMonoid";
"AddCommGroup" -> "AddCommMonoid";
"AddCommGroup" -> "AddGroup";
"AddCommGroup" -> "SubtractionCommMonoid";
"DivisionMonoid" -> "DivInvOneMonoid";
"DivisionMonoid" -> "InvolutiveInv";
"DivisionMonoid" -> "DivInvMonoid";
"RankCondition" -> "InvariantBasisNumber";
"NormedLinearOrderedField" -> "Norm";
"NormedLinearOrderedField" -> "NormedField";
"NormedLinearOrderedField" -> "MetricSpace";
"NormedLinearOrderedField" -> "LinearOrderedField";
"InfSet" -> "Nonempty";
"OrderedSemiring" -> "OrderedAddCommMonoid";
"OrderedSemiring" -> "PartialOrder";
"OrderedSemiring" -> "ZeroLEOneClass";
"OrderedSemiring" -> "Semiring";
"CoheytingAlgebra" -> "GeneralizedCoheytingAlgebra";
"CoheytingAlgebra" -> "DistribLattice";
"CoheytingAlgebra" -> "HNot";
"CoheytingAlgebra" -> "BoundedOrder";
"CoheytingAlgebra" -> "Top";
"Semifield" -> "Nontrivial";
"Semifield" -> "Inv";
"Semifield" -> "Div";
"Semifield" -> "CommSemiring";
"Semifield" -> "DivisionSemiring";
"Semifield" -> "CommGroupWithZero";
"CategoryTheory.Bicategory.Strict" -> "CategoryTheory.Category";
"ContractibleSpace" -> "SimplyConnectedSpace";
"ContractibleSpace" -> "PathConnectedSpace";
"CanonicallyOrderedMonoid" -> "OrderedCommMonoid";
"CanonicallyOrderedMonoid" -> "ExistsMulOfLE";
"CanonicallyOrderedMonoid" -> "OrderBot";
"CanonicallyOrderedMonoid" -> "Bot";
"CompletelyDistribLattice" -> "CompleteDistribLattice";
"CompletelyDistribLattice" -> "CompleteLattice";
"CircularPreorder" -> "Btw";
"CircularPreorder" -> "SBtw";
"CategoryTheory.SplitMonoCategory" -> "CategoryTheory.RegularMonoCategory";
"CompleteBooleanAlgebra" -> "BooleanAlgebra";
"CompleteBooleanAlgebra" -> "CompleteDistribLattice";
"CompleteBooleanAlgebra" -> "InfSet";
"CompleteBooleanAlgebra" -> "SupSet";
"LocalRing" -> "Nontrivial";
"IsSimpleGroup" -> "Nontrivial";
"Setoid" -> "HasEquiv";
"UniqueFactorizationMonoid" -> "WfDvdMonoid";
"CategoryTheory.Limits.HasStrongEpiMonoFactorisations" -> "CategoryTheory.Limits.HasImages";
"CategoryTheory.Limits.HasStrongEpiMonoFactorisations" -> "CategoryTheory.Limits.HasStrongEpiImages";
"TopologicalLattice" -> "ContinuousSup";
"TopologicalLattice" -> "ContinuousInf";
"NonUnitalNormedRing" -> "NonUnitalSeminormedRing";
"NonUnitalNormedRing" -> "Norm";
"NonUnitalNormedRing" -> "MetricSpace";
"NonUnitalNormedRing" -> "NonUnitalRing";
"NonUnitalNormedRing" -> "NormedAddCommGroup";
"NonAssocRing" -> "NonUnitalNonAssocRing";
"NonAssocRing" -> "AddCommGroupWithOne";
"NonAssocRing" -> "One";
"NonAssocRing" -> "IntCast";
"NonAssocRing" -> "NatCast";
"NonAssocRing" -> "NonAssocSemiring";
"LawfulFix" -> "Fix";
"NonUnitalCommRing" -> "CommSemigroup";
"NonUnitalCommRing" -> "NonUnitalRing";
"NonUnitalCommRing" -> "NonUnitalCommSemiring";
"SupSet" -> "Nonempty";
"LinearOrderedAddCommMonoid" -> "OrderedAddCommMonoid";
"LinearOrderedAddCommMonoid" -> "LinearOrder";
"LinearOrderedAddCommMonoid" -> "AddCommMonoid";
"Bot" -> "Nonempty";
"CategoryTheory.Artinian" -> "CategoryTheory.EssentiallySmall";
"CompletableTopField" -> "SeparatedSpace";
"MulZeroOneClass" -> "MulZeroClass";
"MulZeroOneClass" -> "MulOneClass";
"MulZeroOneClass" -> "Zero";
"CommGroup" -> "IsSolvable";
"CommGroup" -> "DivisionCommMonoid";
"CommGroup" -> "Group";
"CommGroup" -> "Group.IsNilpotent";
"CommGroup" -> "CommMonoid";
"CommGroup" -> "CancelCommMonoid";
"DiscreteValuationRing" -> "LocalRing";
"DiscreteValuationRing" -> "IsPrincipalIdealRing";
"DiscreteValuationRing" -> "ValuationRing";
"ProperSpace" -> "CompleteSpace";
"ProperSpace" -> "TopologicalSpace.SecondCountableTopology";
"ProperSpace" -> "LocallyCompactSpace";
"StarSemigroup" -> "InvolutiveStar";
"CategoryTheory.Limits.HasLimitsOfSize" -> "CategoryTheory.Limits.HasFiniteLimits";
"IsEmpty" -> "Fintype";
"IsEmpty" -> "Subsingleton";
"IsEmpty" -> "Encodable";
"Std.ToFormat" -> "Lean.ToMessageData";
"IsCancelMulZero" -> "IsLeftCancelMulZero";
"IsCancelMulZero" -> "IsRightCancelMulZero";
"LinearOrderedCommGroupWithZero" -> "Nontrivial";
"LinearOrderedCommGroupWithZero" -> "Inv";
"LinearOrderedCommGroupWithZero" -> "Div";
"LinearOrderedCommGroupWithZero" -> "LinearOrderedCommMonoidWithZero";
"LinearOrderedCommGroupWithZero" -> "CommGroupWithZero";
"LinearOrderedCancelCommMonoid" -> "Ord";
"LinearOrderedCancelCommMonoid" -> "Max";
"LinearOrderedCancelCommMonoid" -> "Min";
"LinearOrderedCancelCommMonoid" -> "LinearOrderedCommMonoid";
"LinearOrderedCancelCommMonoid" -> "OrderedCancelCommMonoid";
"AddSemigroup" -> "Add";
"LinearOrderedSemifield" -> "Inv";
"LinearOrderedSemifield" -> "LinearOrderedCommSemiring";
"LinearOrderedSemifield" -> "Semifield";
"LinearOrderedSemifield" -> "Div";
"LinearOrderedSemifield" -> "DenselyOrdered";
"RightCancelMonoid" -> "Monoid";
"RightCancelMonoid" -> "One";
"RightCancelMonoid" -> "RightCancelSemigroup";
"OrderedCommRing" -> "CommRing";
"OrderedCommRing" -> "OrderedRing";
"OrderedCommRing" -> "OrderedCommSemiring";
"PseudoEMetricSpace" -> "UniformSpace";
"PseudoEMetricSpace" -> "ParacompactSpace";
"PseudoEMetricSpace" -> "EDist";
"NormedStarGroup" -> "ContinuousStar";
"OrderTop" -> "Top";
"InvolutiveInv" -> "Inv";
"EMetricSpace" -> "SeparatedSpace";
"EMetricSpace" -> "PseudoEMetricSpace";
"EMetricSpace" -> "NormalSpace";
"DivInvMonoid" -> "Monoid";
"DivInvMonoid" -> "Inv";
"DivInvMonoid" -> "Div";
"CircularPartialOrder" -> "CircularPreorder";
"NormedField" -> "NormedCommRing";
"NormedField" -> "Norm";
"NormedField" -> "MetricSpace";
"NormedField" -> "Field";
"NormedField" -> "NormedDivisionRing";
"InvOneClass" -> "One";
"InvOneClass" -> "Inv";
"LeftCancelSemigroup" -> "Semigroup";
"LeftCancelSemigroup" -> "IsLeftCancelMul";
"CompactSpace" -> "ParacompactSpace";
"CompactSpace" -> "SigmaCompactSpace";
"AddCommMonoid" -> "AddMonoid";
"AddCommMonoid" -> "AddCommSemigroup";
"SimplyConnectedSpace" -> "PathConnectedSpace";
"AddGroupFilterBasis" -> "TopologicalAddGroup";
"IsCoatomistic" -> "IsCoatomic";
"CharZero" -> "Nontrivial";
"CharZero" -> "Infinite";
"Lean.Eval" -> "Lean.MetaEval";
"CategoryTheory.Preadditive" -> "CategoryTheory.Limits.HasZeroMorphisms";
"LinearOrderedCommRing" -> "StrictOrderedCommRing";
"LinearOrderedCommRing" -> "LinearOrderedCommSemiring";
"LinearOrderedCommRing" -> "LinearOrderedRing";
"LinearOrderedCommRing" -> "CommMonoid";
"NormedCommGroup" -> "NormedGroup";
"NormedCommGroup" -> "Norm";
"NormedCommGroup" -> "CommGroup";
"NormedCommGroup" -> "MetricSpace";
"NormedCommGroup" -> "SeminormedCommGroup";
"CommSemiring" -> "CommMonoidWithZero";
"CommSemiring" -> "Semiring";
"CommSemiring" -> "NonUnitalCommSemiring";
"CommSemiring" -> "CommMonoid";
"OmegaCompletePartialOrder" -> "PartialOrder";
"CategoryTheory.Limits.HasStrictInitialObjects" -> "CategoryTheory.Limits.InitialMonoClass";
"AddRightCancelMonoid" -> "AddRightCancelSemigroup";
"AddRightCancelMonoid" -> "AddMonoid";
"AddRightCancelMonoid" -> "Zero";
"CommSemigroup" -> "Semigroup";
"CommSemigroup" -> "IsCommJordan";
"IdemCommSemiring" -> "CommSemiring";
"IdemCommSemiring" -> "IdemSemiring";
"IdemCommSemiring" -> "SemilatticeSup";
"DivisionSemiring" -> "Nontrivial";
"DivisionSemiring" -> "Inv";
"DivisionSemiring" -> "GroupWithZero";
"DivisionSemiring" -> "Div";
"DivisionSemiring" -> "Semiring";
"OrderedCommSemiring" -> "OrderedSemiring";
"OrderedCommSemiring" -> "CommSemiring";
"CategoryTheory.Bicategory" -> "CategoryTheory.CategoryStruct";
"DistribLattice" -> "Lattice";
"DistribLattice" -> "IsModularLattice";
"LieRing" -> "AddCommGroup";
"InvolutiveNeg" -> "Neg";
"PseudoMetricSpace" -> "TopologicalSpace.PseudoMetrizableSpace";
"PseudoMetricSpace" -> "UniformSpace";
"PseudoMetricSpace" -> "NNDist";
"PseudoMetricSpace" -> "PseudoEMetricSpace";
"PseudoMetricSpace" -> "Dist";
"PseudoMetricSpace" -> "EDist";
"PseudoMetricSpace" -> "Bornology";
"AddGroup" -> "SubNegMonoid";
"AddGroup" -> "AddCancelMonoid";
"AddGroup" -> "SubtractionMonoid";
"AddZeroClass" -> "Add";
"AddZeroClass" -> "Zero";
"SemilatticeInf" -> "PartialOrder";
"SemilatticeInf" -> "CategoryTheory.IsCofilteredOrEmpty";
"SemilatticeInf" -> "Inf";
"MeasurableSup₂" -> "MeasurableSup";
"MonoidWithZero" -> "Monoid";
"MonoidWithZero" -> "SemigroupWithZero";
"MonoidWithZero" -> "MulZeroOneClass";
"MonoidWithZero" -> "Zero";
"LeftCancelMonoid" -> "Monoid";
"LeftCancelMonoid" -> "One";
"LeftCancelMonoid" -> "LeftCancelSemigroup";
"SubNegZeroMonoid" -> "SubNegMonoid";
"SubNegZeroMonoid" -> "NegZeroClass";
"NonAssocSemiring" -> "One";
"NonAssocSemiring" -> "AddCommMonoidWithOne";
"NonAssocSemiring" -> "NatCast";
"NonAssocSemiring" -> "MulZeroOneClass";
"NonAssocSemiring" -> "NonUnitalNonAssocSemiring";
"DenselyNormedField" -> "NormedField";
"DenselyNormedField" -> "NontriviallyNormedField";
"UnitalShelf" -> "One";
"UnitalShelf" -> "Shelf";
"StarOrderedRing" -> "OrderedAddCommMonoid";
"StarOrderedRing" -> "ExistsAddOfLE";
"StarOrderedRing" -> "StarRing";
"Fintype" -> "Finite";
"Fintype" -> "Small";
"AddRightCancelSemigroup" -> "IsRightCancelAdd";
"AddRightCancelSemigroup" -> "AddSemigroup";
"MetricSpace" -> "SeparatedSpace";
"MetricSpace" -> "TopologicalSpace.MetrizableSpace";
"MetricSpace" -> "EMetricSpace";
"MetricSpace" -> "PseudoMetricSpace";
"NonarchimedeanGroup" -> "TopologicalGroup";
"CategoryTheory.EssentiallySmall" -> "CategoryTheory.LocallySmall";
"Order.Coframe" -> "DistribLattice";
"Order.Coframe" -> "CompleteLattice";
"NormalSpace" -> "T1Space";
"NormalSpace" -> "T3Space";
"LinearOrderedAddCommMonoidWithTop" -> "LinearOrderedAddCommMonoid";
"LinearOrderedAddCommMonoidWithTop" -> "OrderTop";
"LinearOrderedAddCommMonoidWithTop" -> "Top";
"SubtractionMonoid" -> "SubNegMonoid";
"SubtractionMonoid" -> "InvolutiveNeg";
"SubtractionMonoid" -> "SubNegZeroMonoid";
"LinearOrderedCommMonoidWithZero" -> "ZeroLEOneClass";
"LinearOrderedCommMonoidWithZero" -> "CommMonoidWithZero";
"LinearOrderedCommMonoidWithZero" -> "LinearOrderedCommMonoid";
"LinearOrderedCommMonoidWithZero" -> "Zero";
"CategoryTheory.SymmetricCategory" -> "CategoryTheory.BraidedCategory";
"NonUnitalSemiring" -> "SemigroupWithZero";
"NonUnitalSemiring" -> "NonUnitalNonAssocSemiring";
"CategoryTheory.NormalMonoCategory" -> "CategoryTheory.RegularMonoCategory";
"CanonicallyOrderedAddMonoid" -> "OrderedAddCommMonoid";
"CanonicallyOrderedAddMonoid" -> "OrderBot";
"CanonicallyOrderedAddMonoid" -> "Bot";
"CanonicallyOrderedAddMonoid" -> "ExistsAddOfLE";
"CanonicallyLinearOrderedAddMonoid" -> "Ord";
"CanonicallyLinearOrderedAddMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedAddMonoid" -> "Max";
"CanonicallyLinearOrderedAddMonoid" -> "Min";
"CanonicallyLinearOrderedAddMonoid" -> "CanonicallyOrderedAddMonoid";
"CanonicallyLinearOrderedAddMonoid" -> "SemilatticeSup";
"StarRing" -> "StarSemigroup";
"StarRing" -> "StarAddMonoid";
"CommMonoidWithZero" -> "MonoidWithZero";
"CommMonoidWithZero" -> "CommMonoid";
"CommMonoidWithZero" -> "Zero";
"StrongRankCondition" -> "RankCondition";
"GeneralizedBooleanAlgebra" -> "GeneralizedCoheytingAlgebra";
"GeneralizedBooleanAlgebra" -> "OrderBot";
"GeneralizedBooleanAlgebra" -> "Bot";
"GeneralizedBooleanAlgebra" -> "DistribLattice";
"GeneralizedBooleanAlgebra" -> "SDiff";
"T2Space" -> "QuasiSober";
"T2Space" -> "T1Space";
"T2Space" -> "QuasiSeparatedSpace";
"EuclideanDomain" -> "Mod";
"EuclideanDomain" -> "Nontrivial";
"EuclideanDomain" -> "IsDomain";
"EuclideanDomain" -> "CommRing";
"EuclideanDomain" -> "Div";
"EuclideanDomain" -> "NoZeroDivisors";
"EuclideanDomain" -> "IsPrincipalIdealRing";
"OrderedCancelAddCommMonoid" -> "OrderedAddCommMonoid";
"OrderedCancelAddCommMonoid" -> "AddCancelCommMonoid";
"OrderedCancelAddCommMonoid" -> "PartialOrder";
"OrderedCancelAddCommMonoid" -> "AddCommMonoid";
"TotallySeparatedSpace" -> "TotallyDisconnectedSpace";
"Distrib" -> "Mul";
"Distrib" -> "LeftDistribClass";
"Distrib" -> "Add";
"Distrib" -> "RightDistribClass";
"LinearOrderedAddCommGroup" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedAddCommGroup" -> "Ord";
"LinearOrderedAddCommGroup" -> "LinearOrder";
"LinearOrderedAddCommGroup" -> "Max";
"LinearOrderedAddCommGroup" -> "Min";
"LinearOrderedAddCommGroup" -> "OrderedAddCommGroup";
"MeasurableDiv₂" -> "MeasurableDiv";
"CommGroupWithZero" -> "Nontrivial";
"CommGroupWithZero" -> "Inv";
"CommGroupWithZero" -> "CancelCommMonoidWithZero";
"CommGroupWithZero" -> "DivisionCommMonoid";
"CommGroupWithZero" -> "GroupWithZero";
"CommGroupWithZero" -> "Div";
"CommGroupWithZero" -> "CommMonoidWithZero";
"ToString" -> "Std.ToFormat";
"ToString" -> "Lean.Eval";
"AddMonoid" -> "AddSemigroup";
"AddMonoid" -> "AddZeroClass";
"AddMonoid" -> "Zero";
"T5Space" -> "NormalSpace";
"T5Space" -> "T1Space";
"CategoryTheory.Limits.HasZeroObject" -> "CategoryTheory.Limits.InitialMonoClass";
"NormedLinearOrderedAddGroup" -> "Norm";
"NormedLinearOrderedAddGroup" -> "MetricSpace";
"NormedLinearOrderedAddGroup" -> "LinearOrderedAddCommGroup";
"NormedLinearOrderedAddGroup" -> "NormedOrderedAddGroup";
"IsCancelAdd" -> "IsRightCancelAdd";
"IsCancelAdd" -> "IsLeftCancelAdd";
"CategoryTheory.Adhesive" -> "CategoryTheory.RegularMonoCategory";
"LinearOrderedCommMonoid" -> "OrderedCommMonoid";
"LinearOrderedCommMonoid" -> "LinearOrder";
"LinearOrderedCommMonoid" -> "CommMonoid";
"CategoryTheory.RigidCategory" -> "CategoryTheory.RightRigidCategory";
"CategoryTheory.RigidCategory" -> "CategoryTheory.LeftRigidCategory";
"TopologicalSpace.SecondCountableTopology" -> "TopologicalSpace.FirstCountableTopology";
"TopologicalSpace.SecondCountableTopology" -> "TopologicalSpace.SeparableSpace";
"MeasurableAdd₂" -> "MeasurableAdd";
"CancelMonoid" -> "IsCancelMul";
"CancelMonoid" -> "RightCancelMonoid";
"CancelMonoid" -> "LeftCancelMonoid";
"CategoryTheory.IsConnected" -> "CategoryTheory.IsPreconnected";
"CategoryTheory.IsConnected" -> "Nonempty";
"IsAlgClosed" -> "Infinite";
"PolishSpace" -> "T2Space";
"Primcodable" -> "Encodable";
"HasDistribNeg" -> "InvolutiveNeg";
"IsDedekindDomain" -> "IsIntegrallyClosed";
"IsDedekindDomain" -> "Ring.DimensionLEOne";
"Semiring" -> "One";
"Semiring" -> "NatCast";
"Semiring" -> "MonoidWithZero";
"Semiring" -> "NonAssocSemiring";
"Semiring" -> "NonUnitalSemiring";
"StarAddMonoid" -> "InvolutiveStar";
"NontriviallyNormedField" -> "NormedField";
"NontriviallyNormedField" -> "NoncompactSpace";
"Countable" -> "Small";
"HenselianLocalRing" -> "LocalRing";
"CompleteLinearOrder" -> "LinearOrder";
"CompleteLinearOrder" -> "ConditionallyCompleteLinearOrderBot";
"CompleteLinearOrder" -> "CompletelyDistribLattice";
"CompleteLinearOrder" -> "CompleteLattice";
"Inhabited" -> "Nonempty";
"CategoryTheory.IsFiltered" -> "CategoryTheory.IsFilteredOrEmpty";
"Subsingleton" -> "Finite";
"Subsingleton" -> "Countable";
"Subsingleton" -> "Small";
"TopologicalSpace.NoetherianSpace" -> "CompactSpace";
"TopologicalSpace.NoetherianSpace" -> "QuasiSeparatedSpace";
"FinEnum" -> "Fintype";
"CompleteSemilatticeInf" -> "PartialOrder";
"CompleteSemilatticeInf" -> "InfSet";
"IsModularLattice" -> "IsLowerModularLattice";
"IsModularLattice" -> "IsUpperModularLattice";
"AddGroupWithOne" -> "IntCast";
"AddGroupWithOne" -> "Neg";
"AddGroupWithOne" -> "AddGroup";
"AddGroupWithOne" -> "AddMonoidWithOne";
"AddGroupWithOne" -> "Sub";
"CategoryTheory.CategoryStruct" -> "Quiver";
"StrictOrderedRing" -> "Nontrivial";
"StrictOrderedRing" -> "StrictOrderedSemiring";
"StrictOrderedRing" -> "OrderedRing";
"StrictOrderedRing" -> "PartialOrder";
"StrictOrderedRing" -> "OrderedAddCommGroup";
"StrictOrderedRing" -> "Ring";
"DivisionRing" -> "Nontrivial";
"DivisionRing" -> "IsDomain";
"DivisionRing" -> "Inv";
"DivisionRing" -> "OfScientific";
"DivisionRing" -> "Div";
"DivisionRing" -> "DivInvMonoid";
"DivisionRing" -> "DivisionSemiring";
"DivisionRing" -> "RatCast";
"DivisionRing" -> "IsPrincipalIdealRing";
"DivisionRing" -> "Ring";
"IrreducibleSpace" -> "Nonempty";
"IrreducibleSpace" -> "ConnectedSpace";
"IrreducibleSpace" -> "PreirreducibleSpace";
"Quiver.HasInvolutiveReverse" -> "Quiver.HasReverse";
"NormedOrderedAddGroup" -> "Norm";
"NormedOrderedAddGroup" -> "MetricSpace";
"NormedOrderedAddGroup" -> "OrderedAddCommGroup";
"NormedOrderedAddGroup" -> "NormedAddCommGroup";
"Infinite" -> "Nontrivial";
"SizeOf" -> "WellFoundedRelation";
"CstarRing" -> "NormedStarGroup";
"NormedOrderedGroup" -> "OrderedCommGroup";
"NormedOrderedGroup" -> "Norm";
"NormedOrderedGroup" -> "NormedCommGroup";
"NormedOrderedGroup" -> "MetricSpace";
"IsSimpleAddGroup" -> "Nontrivial";
"Group.IsNilpotent" -> "IsSolvable";
"NonUnitalRing" -> "NonUnitalNonAssocRing";
"NonUnitalRing" -> "NonUnitalSemiring";
"NonUnitalCommSemiring" -> "CommSemigroup";
"NonUnitalCommSemiring" -> "NonUnitalSemiring";
"HeytingAlgebra" -> "HasCompl";
"HeytingAlgebra" -> "Bot";
"HeytingAlgebra" -> "BoundedOrder";
"HeytingAlgebra" -> "GeneralizedHeytingAlgebra";
"NormedLinearOrderedGroup" -> "LinearOrderedCommGroup";
"NormedLinearOrderedGroup" -> "Norm";
"NormedLinearOrderedGroup" -> "MetricSpace";
"NormedLinearOrderedGroup" -> "NormedOrderedGroup";
"ConditionallyCompleteLinearOrder" -> "LinearOrder";
"ConditionallyCompleteLinearOrder" -> "ConditionallyCompleteLattice";
"Order.Frame" -> "DistribLattice";
"Order.Frame" -> "CompleteLattice";
"AddCommSemigroup" -> "AddSemigroup";
"ValuationRing" -> "IsBezout";
"ValuationRing" -> "LocalRing";
"T1Space" -> "T0Space";
"SeminormedCommGroup" -> "TopologicalGroup";
"SeminormedCommGroup" -> "SeminormedGroup";
"SeminormedCommGroup" -> "LipschitzMul";
"SeminormedCommGroup" -> "UniformGroup";
"SeminormedCommGroup" -> "Norm";
"SeminormedCommGroup" -> "CommGroup";
"SeminormedCommGroup" -> "PseudoMetricSpace";
"IsAtomistic" -> "IsAtomic";
"MulOneClass" -> "One";
"MulOneClass" -> "Mul";
"SubtractionCommMonoid" -> "AddCommMonoid";
"SubtractionCommMonoid" -> "SubtractionMonoid";
"Denumerable" -> "Primcodable";
"Denumerable" -> "Infinite";
"Denumerable" -> "Encodable";
"RightCancelSemigroup" -> "Semigroup";
"RightCancelSemigroup" -> "IsRightCancelMul";
"NonUnitalNonAssocSemiring" -> "Mul";
"NonUnitalNonAssocSemiring" -> "MulZeroClass";
"NonUnitalNonAssocSemiring" -> "AddCommMonoid";
"NonUnitalNonAssocSemiring" -> "Distrib";
"BoundedOrder" -> "OrderBot";
"BoundedOrder" -> "OrderTop";
"NegZeroClass" -> "Neg";
"NegZeroClass" -> "Zero";
"OrderedAddCommGroup" -> "PartialOrder";
"OrderedAddCommGroup" -> "AddCommGroup";
"OrderedAddCommGroup" -> "OrderedCancelAddCommMonoid";
"StrictOrderedCommSemiring" -> "StrictOrderedSemiring";
"StrictOrderedCommSemiring" -> "CommSemiring";
"StrictOrderedCommSemiring" -> "OrderedCommSemiring";
"CompleteLattice" -> "Lattice";
"CompleteLattice" -> "CompleteSemilatticeSup";
"CompleteLattice" -> "ConditionallyCompleteLattice";
"CompleteLattice" -> "InfSet";
"CompleteLattice" -> "SupSet";
"CompleteLattice" -> "Bot";
"CompleteLattice" -> "OmegaCompletePartialOrder";
"CompleteLattice" -> "CompleteSemilatticeInf";
"CompleteLattice" -> "BoundedOrder";
"CompleteLattice" -> "Top";
"T3Space" -> "RegularSpace";
"T3Space" -> "T0Space";
"T3Space" -> "T25Space";
"FloorRing" -> "FloorSemiring";
"CategoryTheory.SplitEpiCategory" -> "CategoryTheory.RegularEpiCategory";
"TopologicalRing" -> "ContinuousNeg";
"TopologicalRing" -> "TopologicalAddGroup";
"TopologicalRing" -> "TopologicalSemiring";
"ConnectedSpace" -> "PreconnectedSpace";
"ConnectedSpace" -> "Nonempty";
"TopologicalAddGroup" -> "RegularSpace";
"TopologicalAddGroup" -> "HSpace";
"TopologicalAddGroup" -> "ContinuousSub";
"TopologicalAddGroup" -> "ContinuousNeg";
"TopologicalAddGroup" -> "ContinuousAdd";
"Repr" -> "ReprTuple";
"Repr" -> "Lean.Eval";
"OrderedCancelCommMonoid" -> "OrderedCommMonoid";
"OrderedCancelCommMonoid" -> "PartialOrder";
"OrderedCancelCommMonoid" -> "CommMonoid";
"OrderedCancelCommMonoid" -> "CancelCommMonoid";
"CategoryTheory.NormalEpiCategory" -> "CategoryTheory.RegularEpiCategory";
"LinearOrderedSemiring" -> "StrictOrderedSemiring";
"LinearOrderedSemiring" -> "Ord";
"LinearOrderedSemiring" -> "Max";
"LinearOrderedSemiring" -> "LinearOrderedAddCommMonoid";
"LinearOrderedSemiring" -> "Min";
"IdemSemiring" -> "OrderBot";
"IdemSemiring" -> "CanonicallyOrderedAddMonoid";
"IdemSemiring" -> "Semiring";
"IdemSemiring" -> "SemilatticeSup";
"CommMonoid" -> "Monoid";
"CommMonoid" -> "CommSemigroup";
"SemilatticeSup" -> "PartialOrder";
"SemilatticeSup" -> "Sup";
"SemilatticeSup" -> "CategoryTheory.IsFilteredOrEmpty";
"CategoryTheory.Limits.HasFiniteColimits" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"Field" -> "Nontrivial";
"Field" -> "IsDomain";
"Field" -> "CommRing";
"Field" -> "Inv";
"Field" -> "Semifield";
"Field" -> "Div";
"Field" -> "LocalRing";
"Field" -> "RatCast";
"Field" -> "EuclideanDomain";
"Field" -> "HenselianLocalRing";
"Field" -> "DivisionRing";
"Field" -> "ValuationRing";
"Field" -> "Ideal.IsJacobson";
"CategoryTheory.StrongMonoCategory" -> "CategoryTheory.Balanced";
"Ring" -> "IntCast";
"Ring" -> "AddCommGroup";
"Ring" -> "NonAssocRing";
"Ring" -> "LieRing";
"Ring" -> "Neg";
"Ring" -> "Semiring";
"Ring" -> "AddGroupWithOne";
"Ring" -> "NonUnitalRing";
"Ring" -> "Sub";
"T25Space" -> "T2Space";
"NumberField" -> "CharZero";
"NonarchimedeanRing" -> "NonarchimedeanAddGroup";
"NonarchimedeanRing" -> "TopologicalRing";
"GeneralizedHeytingAlgebra" -> "Lattice";
"GeneralizedHeytingAlgebra" -> "HImp";
"GeneralizedHeytingAlgebra" -> "OrderTop";
"GeneralizedHeytingAlgebra" -> "DistribLattice";
"GeneralizedHeytingAlgebra" -> "Top";
"MeasureTheory.MeasureSpace" -> "MeasurableSpace";
"NormedRing" -> "Norm";
"NormedRing" -> "NonUnitalNormedRing";
"NormedRing" -> "MetricSpace";
"NormedRing" -> "Ring";
"NormedRing" -> "SeminormedRing";
"NonemptyFinLinOrd" -> "LinearOrder";
"NonemptyFinLinOrd" -> "Fintype";
"NonemptyFinLinOrd" -> "Nonempty";
"NonemptyFinLinOrd" -> "BoundedOrder";
"CanonicallyOrderedCommSemiring" -> "OrderedCommMonoid";
"CanonicallyOrderedCommSemiring" -> "One";
"CanonicallyOrderedCommSemiring" -> "Mul";
"CanonicallyOrderedCommSemiring" -> "NatCast";
"CanonicallyOrderedCommSemiring" -> "CommSemiring";
"CanonicallyOrderedCommSemiring" -> "OrderedCommSemiring";
"CanonicallyOrderedCommSemiring" -> "NoZeroDivisors";
"CanonicallyOrderedCommSemiring" -> "CanonicallyOrderedAddMonoid";
"CategoryTheory.Limits.HasStrongEpiImages" -> "CategoryTheory.Limits.HasImageMaps";
"Top" -> "Nonempty";
"SeminormedRing" -> "NonUnitalSeminormedRing";
"SeminormedRing" -> "Norm";
"SeminormedRing" -> "PseudoMetricSpace";
"SeminormedRing" -> "Ring";
"NormedDivisionRing" -> "NormOneClass";
"NormedDivisionRing" -> "TopologicalDivisionRing";
"NormedDivisionRing" -> "HasContinuousInv₀";
"NormedDivisionRing" -> "Norm";
"NormedDivisionRing" -> "MetricSpace";
"NormedDivisionRing" -> "DivisionRing";
"NormedDivisionRing" -> "NormedRing";
"CancelMonoidWithZero" -> "IsCancelMulZero";
"CancelMonoidWithZero" -> "MonoidWithZero";
"CancelMonoidWithZero" -> "NoZeroDivisors";
"LinearOrderedField" -> "Inv";
"LinearOrderedField" -> "Div";
"LinearOrderedField" -> "LinearOrderedSemifield";
"LinearOrderedField" -> "LinearOrderedCommRing";
"LinearOrderedField" -> "RatCast";
"LinearOrderedField" -> "Field";
"TopologicalSemiring" -> "ContinuousMul";
"TopologicalSemiring" -> "ContinuousAdd";
"Encodable" -> "Countable";
"CircularOrder" -> "CircularPartialOrder";
"MeasurableMul₂" -> "MeasurableMul";
"Preorder" -> "LE";
"Preorder" -> "LT";
"BooleanRing" -> "CommRing";
"BooleanRing" -> "Ring";
"CategoryTheory.StrongEpiCategory" -> "CategoryTheory.Balanced";
"NormedAddCommGroup" -> "SeminormedAddCommGroup";
"NormedAddCommGroup" -> "AddCommGroup";
"NormedAddCommGroup" -> "Norm";
"NormedAddCommGroup" -> "MetricSpace";
"NormedAddCommGroup" -> "NormedAddGroup";
"AddMonoidWithOne" -> "One";
"AddMonoidWithOne" -> "NatCast";
"AddMonoidWithOne" -> "AddMonoid";
"PathConnectedSpace" -> "ConnectedSpace";
"CategoryTheory.Category" -> "CategoryTheory.CategoryStruct";
"PreirreducibleSpace" -> "PreconnectedSpace";
"CanonicallyLinearOrderedMonoid" -> "Ord";
"CanonicallyLinearOrderedMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedMonoid" -> "Max";
"CanonicallyLinearOrderedMonoid" -> "CanonicallyOrderedMonoid";
"CanonicallyLinearOrderedMonoid" -> "Min";
"CanonicallyLinearOrderedMonoid" -> "SemilatticeSup";
"FrechetUrysohnSpace" -> "SequentialSpace";
"NormedAddGroup" -> "SeminormedAddGroup";
"NormedAddGroup" -> "Norm";
"NormedAddGroup" -> "AddGroup";
"NormedAddGroup" -> "MetricSpace";
"CancelCommMonoid" -> "LeftCancelMonoid";
"CancelCommMonoid" -> "CancelMonoid";
"CancelCommMonoid" -> "CommMonoid";
"Zero" -> "Nonempty";
"UniformAddGroup" -> "TopologicalAddGroup";
"SeparatedSpace" -> "UniformSpace" [style=dashed];
"TopologicalSpace.PseudoMetrizableSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.IsPreconnected" -> "CategoryTheory.Category" [style=dashed];
"NormOneClass" -> "One" [style=dashed];
"NormOneClass" -> "Norm" [style=dashed];
"CategoryTheory.RegularMonoCategory" -> "CategoryTheory.Category" [style=dashed];
"MeasurableInf₂" -> "MeasurableSpace" [style=dashed];
"MeasurableInf₂" -> "Inf" [style=dashed];
"NonarchimedeanAddGroup" -> "TopologicalSpace" [style=dashed];
"NonarchimedeanAddGroup" -> "AddGroup" [style=dashed];
"CategoryTheory.Limits.HasZeroMorphisms" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.IsIdempotentComplete" -> "CategoryTheory.Category" [style=dashed];
"IsDomain" -> "Semiring" [style=dashed];
"IsRightCancelAdd" -> "Add" [style=dashed];
"ExistsMulOfLE" -> "Mul" [style=dashed];
"ExistsMulOfLE" -> "LE" [style=dashed];
"AddMonoid.FG" -> "AddMonoid" [style=dashed];
"OrderTopology" -> "TopologicalSpace" [style=dashed];
"OrderTopology" -> "Preorder" [style=dashed];
"LipschitzAdd" -> "PseudoMetricSpace" [style=dashed];
"LipschitzAdd" -> "AddMonoid" [style=dashed];
"TopologicalDivisionRing" -> "TopologicalSpace" [style=dashed];
"TopologicalDivisionRing" -> "DivisionRing" [style=dashed];
"CategoryTheory.Noetherian" -> "CategoryTheory.Category" [style=dashed];
"HasUpperLowerClosure" -> "TopologicalSpace" [style=dashed];
"HasUpperLowerClosure" -> "Preorder" [style=dashed];
"CompleteSpace" -> "UniformSpace" [style=dashed];
"IsSolvable" -> "Group" [style=dashed];
"TopologicalSpace.MetrizableSpace" -> "TopologicalSpace" [style=dashed];
"IsFreeGroupoid" -> "CategoryTheory.Groupoid" [style=dashed];
"GCDMonoid" -> "CancelCommMonoidWithZero" [style=dashed];
"LocallyFiniteOrderTop" -> "Preorder" [style=dashed];
"CategoryTheory.RegularEpiCategory" -> "CategoryTheory.Category" [style=dashed];
"TopologicalGroup" -> "Group" [style=dashed];
"TopologicalGroup" -> "TopologicalSpace" [style=dashed];
"Quiver.Arborescence" -> "Quiver" [style=dashed];
"CategoryTheory.Limits.HasFiniteWidePullbacks" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasImages" -> "CategoryTheory.Category" [style=dashed];
"RegularSpace" -> "TopologicalSpace" [style=dashed];
"TopologicalSpace.FirstCountableTopology" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.IsCofiltered" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.LocallySmall" -> "CategoryTheory.Category" [style=dashed];
"IsLowerModularLattice" -> "Lattice" [style=dashed];
"NoMinOrder" -> "LT" [style=dashed];
"MeasurableDiv" -> "Div" [style=dashed];
"MeasurableDiv" -> "MeasurableSpace" [style=dashed];
"CategoryTheory.FinitaryExtensive" -> "CategoryTheory.Category" [style=dashed];
"DiscreteTopology" -> "TopologicalSpace" [style=dashed];
"ContinuousStar" -> "TopologicalSpace" [style=dashed];
"ContinuousStar" -> "Star" [style=dashed];
"NoMaxOrder" -> "LT" [style=dashed];
"NormalizationMonoid" -> "CancelCommMonoidWithZero" [style=dashed];
"MeasurableSingletonClass" -> "MeasurableSpace" [style=dashed];
"CategoryTheory.HasInjectiveResolutions" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.HasInjectiveResolutions" -> "CategoryTheory.Limits.HasImages" [style=dashed];
"CategoryTheory.HasInjectiveResolutions" -> "CategoryTheory.Limits.HasEqualizers" [style=dashed];
"CategoryTheory.HasInjectiveResolutions" -> "CategoryTheory.Limits.HasZeroObject" [style=dashed];
"CategoryTheory.HasInjectiveResolutions" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasFiniteLimits" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.MonoidalCategory" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Category" [style=dashed];
"IsCompactlyGenerated" -> "CompleteLattice" [style=dashed];
"BoundedRandom" -> "Preorder" [style=dashed];
"NormalizedGCDMonoid" -> "CancelCommMonoidWithZero" [style=dashed];
"HSpace" -> "TopologicalSpace" [style=dashed];
"PreconnectedSpace" -> "TopologicalSpace" [style=dashed];
"IsSimpleOrder" -> "LE" [style=dashed];
"IsSimpleOrder" -> "BoundedOrder" [style=dashed];
"CategoryTheory.MonoidalPreadditive" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.MonoidalPreadditive" -> "CategoryTheory.Preadditive" [style=dashed];
"CategoryTheory.MonoidalPreadditive" -> "CategoryTheory.Category" [style=dashed];
"Group.FG" -> "Group" [style=dashed];
"IsCancelMul" -> "Mul" [style=dashed];
"CategoryTheory.Limits.HasColimitsOfSize" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Category" [style=dashed];
"WithIdeal" -> "CommRing" [style=dashed];
"InvariantBasisNumber" -> "Semiring" [style=dashed];
"IsLeftCancelMul" -> "Mul" [style=dashed];
"MeasurableSub₂" -> "MeasurableSpace" [style=dashed];
"MeasurableSub₂" -> "Sub" [style=dashed];
"GroupFilterBasis" -> "Group" [style=dashed];
"UniqueProds" -> "Mul" [style=dashed];
"IsCommJordan" -> "Mul" [style=dashed];
"CategoryTheory.Abelian" -> "CategoryTheory.Category" [style=dashed];
"WStarAlgebra" -> "StarRing" [style=dashed];
"WStarAlgebra" -> "CstarRing" [style=dashed];
"WStarAlgebra" -> "StarModule" [style=dashed];
"WStarAlgebra" -> "Module" [style=dashed];
"WStarAlgebra" -> "NormedAlgebra" [style=dashed];
"WStarAlgebra" -> "NormedRing" [style=dashed];
"OrderBot" -> "LE" [style=dashed];
"LawfulBEq" -> "BEq" [style=dashed];
"LipschitzMul" -> "Monoid" [style=dashed];
"LipschitzMul" -> "PseudoMetricSpace" [style=dashed];
"RingFilterBasis" -> "Ring" [style=dashed];
"IsUpperModularLattice" -> "Lattice" [style=dashed];
"UniformConvexSpace" -> "SeminormedAddCommGroup" [style=dashed];
"BorelSpace" -> "MeasurableSpace" [style=dashed];
"BorelSpace" -> "TopologicalSpace" [style=dashed];
"HasContinuousInv₀" -> "Inv" [style=dashed];
"HasContinuousInv₀" -> "TopologicalSpace" [style=dashed];
"HasContinuousInv₀" -> "Zero" [style=dashed];
"LocallyFiniteOrderBot" -> "Preorder" [style=dashed];
"CategoryTheory.Limits.HasFiniteWidePushouts" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasImageMaps" -> "CategoryTheory.Limits.HasImages" [style=dashed];
"CategoryTheory.Limits.HasImageMaps" -> "CategoryTheory.Category" [style=dashed];
"UniformGroup" -> "UniformSpace" [style=dashed];
"UniformGroup" -> "Group" [style=dashed];
"CategoryTheory.Limits.HasStrictTerminalObjects" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasFiniteCoproducts" -> "CategoryTheory.Category" [style=dashed];
"RankCondition" -> "Semiring" [style=dashed];
"InnerProductSpaceable" -> "NormedAddCommGroup" [style=dashed];
"CategoryTheory.IsTriangulated" -> "CategoryTheory.Preadditive" [style=dashed];
"CategoryTheory.IsTriangulated" -> "CategoryTheory.Limits.HasZeroObject" [style=dashed];
"CategoryTheory.IsTriangulated" -> "CategoryTheory.Pretriangulated" [style=dashed];
"CategoryTheory.IsTriangulated" -> "CategoryTheory.HasShift" [style=dashed];
"CategoryTheory.IsTriangulated" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Bicategory.Strict" -> "CategoryTheory.Bicategory" [style=dashed];
"ContractibleSpace" -> "TopologicalSpace" [style=dashed];
"IsBezout" -> "CommRing" [style=dashed];
"CategoryTheory.SplitMonoCategory" -> "CategoryTheory.Category" [style=dashed];
"BaireSpace" -> "TopologicalSpace" [style=dashed];
"OrderedSub" -> "LE" [style=dashed];
"OrderedSub" -> "Add" [style=dashed];
"OrderedSub" -> "Sub" [style=dashed];
"ZeroLEOneClass" -> "One" [style=dashed];
"ZeroLEOneClass" -> "LE" [style=dashed];
"ZeroLEOneClass" -> "Zero" [style=dashed];
"LocalRing" -> "Semiring" [style=dashed];
"IsSimpleGroup" -> "Group" [style=dashed];
"UniqueFactorizationMonoid" -> "CancelCommMonoidWithZero" [style=dashed];
"CategoryTheory.Limits.HasStrongEpiMonoFactorisations" -> "CategoryTheory.Category" [style=dashed];
"Monoid.FG" -> "Monoid" [style=dashed];
"Lean.Export.OfState" -> "Hashable" [style=dashed];
"Lean.Export.OfState" -> "BEq" [style=dashed];
"TopologicalLattice" -> "Lattice" [style=dashed];
"TopologicalLattice" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Limits.HasReflexiveCoequalizers" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.IsCofilteredOrEmpty" -> "CategoryTheory.Category" [style=dashed];
"LawfulFix" -> "OmegaCompletePartialOrder" [style=dashed];
"IsAtomic" -> "OrderBot" [style=dashed];
"IsAtomic" -> "PartialOrder" [style=dashed];
"TotallyDisconnectedSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Artinian" -> "CategoryTheory.Category" [style=dashed];
"CompletableTopField" -> "UniformSpace" [style=dashed];
"CompletableTopField" -> "Field" [style=dashed];
"CategoryTheory.Limits.HasCoreflexiveEqualizers" -> "CategoryTheory.Category" [style=dashed];
"DiscreteValuationRing" -> "IsDomain" [style=dashed];
"DiscreteValuationRing" -> "CommRing" [style=dashed];
"ProperSpace" -> "PseudoMetricSpace" [style=dashed];
"NoTopOrder" -> "LE" [style=dashed];
"StarSemigroup" -> "Semigroup" [style=dashed];
"CategoryTheory.EnoughInjectives" -> "CategoryTheory.Category" [style=dashed];
"MeasurableMul" -> "Mul" [style=dashed];
"MeasurableMul" -> "MeasurableSpace" [style=dashed];
"ContinuousSub" -> "TopologicalSpace" [style=dashed];
"ContinuousSub" -> "Sub" [style=dashed];
"CategoryTheory.Limits.HasLimitsOfSize" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasCokernels" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.Limits.HasCokernels" -> "CategoryTheory.Category" [style=dashed];
"IsCancelMulZero" -> "Mul" [style=dashed];
"IsCancelMulZero" -> "Zero" [style=dashed];
"MeasurableSup" -> "MeasurableSpace" [style=dashed];
"MeasurableSup" -> "Sup" [style=dashed];
"SequentialSpace" -> "TopologicalSpace" [style=dashed];
"NormedStarGroup" -> "SeminormedAddCommGroup" [style=dashed];
"NormedStarGroup" -> "StarAddMonoid" [style=dashed];
"OrderTop" -> "LE" [style=dashed];
"HasContDiffBump" -> "NormedSpace" [style=dashed];
"HasContDiffBump" -> "NormedAddCommGroup" [style=dashed];
"ContinuousNeg" -> "TopologicalSpace" [style=dashed];
"ContinuousNeg" -> "Neg" [style=dashed];
"SupConvergenceClass" -> "TopologicalSpace" [style=dashed];
"SupConvergenceClass" -> "Preorder" [style=dashed];
"CompactSpace" -> "TopologicalSpace" [style=dashed];
"LocPathConnectedSpace" -> "TopologicalSpace" [style=dashed];
"SimplyConnectedSpace" -> "TopologicalSpace" [style=dashed];
"AddGroupFilterBasis" -> "AddGroup" [style=dashed];
"CategoryTheory.BraidedCategory" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.BraidedCategory" -> "CategoryTheory.Category" [style=dashed];
"IsCoatomistic" -> "CompleteLattice" [style=dashed];
"CharZero" -> "AddMonoidWithOne" [style=dashed];
"CategoryTheory.Preadditive" -> "CategoryTheory.Category" [style=dashed];
"ExistsAddOfLE" -> "LE" [style=dashed];
"ExistsAddOfLE" -> "Add" [style=dashed];
"MeasurableAdd" -> "MeasurableSpace" [style=dashed];
"MeasurableAdd" -> "Add" [style=dashed];
"QuasiSober" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.HasProjectiveResolutions" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.HasProjectiveResolutions" -> "CategoryTheory.Limits.HasImages" [style=dashed];
"CategoryTheory.HasProjectiveResolutions" -> "CategoryTheory.Limits.HasEqualizers" [style=dashed];
"CategoryTheory.HasProjectiveResolutions" -> "CategoryTheory.Limits.HasZeroObject" [style=dashed];
"CategoryTheory.HasProjectiveResolutions" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasStrictInitialObjects" -> "CategoryTheory.Category" [style=dashed];
"IsLeftCancelMulZero" -> "Mul" [style=dashed];
"IsLeftCancelMulZero" -> "Zero" [style=dashed];
"BoundedSpace" -> "Bornology" [style=dashed];
"Std.HashMap.LawfulHashable" -> "Hashable" [style=dashed];
"Std.HashMap.LawfulHashable" -> "BEq" [style=dashed];
"CategoryTheory.ConcreteCategory" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.MonoidalClosed" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.MonoidalClosed" -> "CategoryTheory.Category" [style=dashed];
"FloorSemiring" -> "OrderedSemiring" [style=dashed];
"IsWeakLowerModularLattice" -> "Lattice" [style=dashed];
"ContinuousMul" -> "Mul" [style=dashed];
"ContinuousMul" -> "TopologicalSpace" [style=dashed];
"IsIntegrallyClosed" -> "IsDomain" [style=dashed];
"IsIntegrallyClosed" -> "CommRing" [style=dashed];
"IsPredArchimedean" -> "PredOrder" [style=dashed];
"IsPredArchimedean" -> "Preorder" [style=dashed];
"MeasurableSub" -> "MeasurableSpace" [style=dashed];
"MeasurableSub" -> "Sub" [style=dashed];
"MeasurableSup₂" -> "MeasurableSpace" [style=dashed];
"MeasurableSup₂" -> "Sup" [style=dashed];
"MeasurableInv" -> "Inv" [style=dashed];
"MeasurableInv" -> "MeasurableSpace" [style=dashed];
"NoZeroDivisors" -> "Mul" [style=dashed];
"NoZeroDivisors" -> "Zero" [style=dashed];
"IsJordan" -> "Mul" [style=dashed];
"StarOrderedRing" -> "PartialOrder" [style=dashed];
"StarOrderedRing" -> "NonUnitalSemiring" [style=dashed];
"CategoryTheory.Limits.HasCofilteredLimitsOfSize" -> "CategoryTheory.Category" [style=dashed];
"NonarchimedeanGroup" -> "Group" [style=dashed];
"NonarchimedeanGroup" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.EssentiallySmall" -> "CategoryTheory.Category" [style=dashed];
"Ring.DimensionLEOne" -> "CommRing" [style=dashed];
"NormalSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.WellPowered" -> "CategoryTheory.Category" [style=dashed];
"NoBotOrder" -> "LE" [style=dashed];
"UniqueSums" -> "Add" [style=dashed];
"ComplementedLattice" -> "Lattice" [style=dashed];
"ComplementedLattice" -> "BoundedOrder" [style=dashed];
"CategoryTheory.SymmetricCategory" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.SymmetricCategory" -> "CategoryTheory.Category" [style=dashed];
"IsLeftCancelAdd" -> "Add" [style=dashed];
"CategoryTheory.NormalMonoCategory" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.NormalMonoCategory" -> "CategoryTheory.Category" [style=dashed];
"LeftDistribClass" -> "Mul" [style=dashed];
"LeftDistribClass" -> "Add" [style=dashed];
"StarRing" -> "NonUnitalSemiring" [style=dashed];
"InfConvergenceClass" -> "TopologicalSpace" [style=dashed];
"InfConvergenceClass" -> "Preorder" [style=dashed];
"StrongRankCondition" -> "Semiring" [style=dashed];
"JordanHolderLattice" -> "Lattice" [style=dashed];
"WfDvdMonoid" -> "CommMonoidWithZero" [style=dashed];
"T2Space" -> "TopologicalSpace" [style=dashed];
"TotallySeparatedSpace" -> "TopologicalSpace" [style=dashed];
"ContinuousInv" -> "Inv" [style=dashed];
"ContinuousInv" -> "TopologicalSpace" [style=dashed];
"LowerTopology" -> "TopologicalSpace" [style=dashed];
"LowerTopology" -> "Preorder" [style=dashed];
"MeasurableDiv₂" -> "Div" [style=dashed];
"MeasurableDiv₂" -> "MeasurableSpace" [style=dashed];
"UpperTopology" -> "TopologicalSpace" [style=dashed];
"UpperTopology" -> "Preorder" [style=dashed];
"CategoryTheory.RightRigidCategory" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.RightRigidCategory" -> "CategoryTheory.Category" [style=dashed];
"T5Space" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Limits.HasZeroObject" -> "CategoryTheory.Category" [style=dashed];
"OpensMeasurableSpace" -> "MeasurableSpace" [style=dashed];
"OpensMeasurableSpace" -> "TopologicalSpace" [style=dashed];
"IsCancelAdd" -> "Add" [style=dashed];
"MeasurableNeg" -> "MeasurableSpace" [style=dashed];
"MeasurableNeg" -> "Neg" [style=dashed];
"PartialEquivBEq" -> "BEq" [style=dashed];
"CategoryTheory.Adhesive" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.CoproductsDisjoint" -> "CategoryTheory.Category" [style=dashed];
"ParacompactSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.RigidCategory" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.RigidCategory" -> "CategoryTheory.Category" [style=dashed];
"TopologicalSpace.SecondCountableTopology" -> "TopologicalSpace" [style=dashed];
"MeasurableAdd₂" -> "MeasurableSpace" [style=dashed];
"MeasurableAdd₂" -> "Add" [style=dashed];
"CategoryTheory.Limits.HasKernels" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.Limits.HasKernels" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.IsConnected" -> "CategoryTheory.Category" [style=dashed];
"IsAlgClosed" -> "Field" [style=dashed];
"PolishSpace" -> "TopologicalSpace" [style=dashed];
"TrivialStar" -> "Star" [style=dashed];
"HasDistribNeg" -> "Mul" [style=dashed];
"IsPrincipalIdealRing" -> "Ring" [style=dashed];
"IsDedekindDomain" -> "IsDomain" [style=dashed];
"IsDedekindDomain" -> "CommRing" [style=dashed];
"StarAddMonoid" -> "AddMonoid" [style=dashed];
"Quiver.HasReverse" -> "Quiver" [style=dashed];
"SeqCompactSpace" -> "TopologicalSpace" [style=dashed];
"LocallyFiniteOrder" -> "Preorder" [style=dashed];
"CategoryTheory.FinCategory" -> "CategoryTheory.SmallCategory" [style=dashed];
"HenselianLocalRing" -> "CommRing" [style=dashed];
"CategoryTheory.Pretriangulated" -> "CategoryTheory.Preadditive" [style=dashed];
"CategoryTheory.Pretriangulated" -> "CategoryTheory.Limits.HasZeroObject" [style=dashed];
"CategoryTheory.Pretriangulated" -> "CategoryTheory.HasShift" [style=dashed];
"CategoryTheory.Pretriangulated" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.IsFiltered" -> "CategoryTheory.Category" [style=dashed];
"ContinuousSup" -> "TopologicalSpace" [style=dashed];
"ContinuousSup" -> "Sup" [style=dashed];
"TopologicalSpace.NoetherianSpace" -> "TopologicalSpace" [style=dashed];
"IsModularLattice" -> "Lattice" [style=dashed];
"IrreducibleSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Limits.HasBinaryBiproducts" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.Limits.HasBinaryBiproducts" -> "CategoryTheory.Category" [style=dashed];
"OrderClosedTopology" -> "TopologicalSpace" [style=dashed];
"OrderClosedTopology" -> "Preorder" [style=dashed];
"Quiver.HasInvolutiveReverse" -> "Quiver" [style=dashed];
"IsFreeGroup" -> "Group" [style=dashed];
"CategoryTheory.EnoughProjectives" -> "CategoryTheory.Category" [style=dashed];
"MeasurableSpace.CountablyGenerated" -> "MeasurableSpace" [style=dashed];
"DenselyOrdered" -> "LT" [style=dashed];
"ContinuousInf" -> "TopologicalSpace" [style=dashed];
"ContinuousInf" -> "Inf" [style=dashed];
"CstarRing" -> "NonUnitalNormedRing" [style=dashed];
"CstarRing" -> "StarRing" [style=dashed];
"IsSimpleAddGroup" -> "AddGroup" [style=dashed];
"CategoryTheory.Balanced" -> "CategoryTheory.Category" [style=dashed];
"Group.IsNilpotent" -> "Group" [style=dashed];
"T0Space" -> "TopologicalSpace" [style=dashed];
"IsSuccArchimedean" -> "SuccOrder" [style=dashed];
"IsSuccArchimedean" -> "Preorder" [style=dashed];
"ValuationRing" -> "IsDomain" [style=dashed];
"ValuationRing" -> "CommRing" [style=dashed];
"T1Space" -> "TopologicalSpace" [style=dashed];
"SuccOrder" -> "Preorder" [style=dashed];
"ContinuousAdd" -> "TopologicalSpace" [style=dashed];
"ContinuousAdd" -> "Add" [style=dashed];
"IsAtomistic" -> "CompleteLattice" [style=dashed];
"HasSolidNorm" -> "Lattice" [style=dashed];
"HasSolidNorm" -> "NormedAddCommGroup" [style=dashed];
"LocallyConnectedSpace" -> "TopologicalSpace" [style=dashed];
"IsCyclic" -> "Group" [style=dashed];
"PredOrder" -> "Preorder" [style=dashed];
"BoundedOrder" -> "LE" [style=dashed];
"T3Space" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Limits.MonoCoprod" -> "CategoryTheory.Category" [style=dashed];
"FloorRing" -> "LinearOrderedRing" [style=dashed];
"ContinuousDiv" -> "Div" [style=dashed];
"ContinuousDiv" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.SplitEpiCategory" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.InitialMonoClass" -> "CategoryTheory.Category" [style=dashed];
"AddGroup.FG" -> "AddGroup" [style=dashed];
"TopologicalRing" -> "NonUnitalNonAssocRing" [style=dashed];
"TopologicalRing" -> "TopologicalSpace" [style=dashed];
"LocallyCompactSpace" -> "TopologicalSpace" [style=dashed];
"ConnectedSpace" -> "TopologicalSpace" [style=dashed];
"TopologicalAddGroup" -> "TopologicalSpace" [style=dashed];
"TopologicalAddGroup" -> "AddGroup" [style=dashed];
"CategoryTheory.NormalEpiCategory" -> "CategoryTheory.Limits.HasZeroMorphisms" [style=dashed];
"CategoryTheory.NormalEpiCategory" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasFiniteProducts" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.Limits.HasFiniteColimits" -> "CategoryTheory.Category" [style=dashed];
"IsAddCyclic" -> "AddGroup" [style=dashed];
"MeasurableInf" -> "MeasurableSpace" [style=dashed];
"MeasurableInf" -> "Inf" [style=dashed];
"CategoryTheory.StrongMonoCategory" -> "CategoryTheory.Category" [style=dashed];
"Ideal.IsJacobson" -> "CommRing" [style=dashed];
"T25Space" -> "TopologicalSpace" [style=dashed];
"NumberField" -> "Field" [style=dashed];
"NonarchimedeanRing" -> "TopologicalSpace" [style=dashed];
"NonarchimedeanRing" -> "Ring" [style=dashed];
"IsRightCancelMul" -> "Mul" [style=dashed];
"CategoryTheory.Limits.HasStrongEpiImages" -> "CategoryTheory.Limits.HasImages" [style=dashed];
"CategoryTheory.Limits.HasStrongEpiImages" -> "CategoryTheory.Category" [style=dashed];
"QuasiSeparatedSpace" -> "TopologicalSpace" [style=dashed];
"IsCoatomic" -> "PartialOrder" [style=dashed];
"IsCoatomic" -> "OrderTop" [style=dashed];
"TopologicalSemiring" -> "TopologicalSpace" [style=dashed];
"TopologicalSemiring" -> "NonUnitalNonAssocSemiring" [style=dashed];
"SigmaCompactSpace" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.Precoherent" -> "CategoryTheory.Category" [style=dashed];
"NoncompactSpace" -> "TopologicalSpace" [style=dashed];
"MeasurableMul₂" -> "Mul" [style=dashed];
"MeasurableMul₂" -> "MeasurableSpace" [style=dashed];
"CategoryTheory.Limits.HasFilteredColimitsOfSize" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.StrongEpiCategory" -> "CategoryTheory.Category" [style=dashed];
"PriestleySpace" -> "TopologicalSpace" [style=dashed];
"PriestleySpace" -> "Preorder" [style=dashed];
"CompactIccSpace" -> "TopologicalSpace" [style=dashed];
"CompactIccSpace" -> "Preorder" [style=dashed];
"IsRightCancelMulZero" -> "Mul" [style=dashed];
"IsRightCancelMulZero" -> "Zero" [style=dashed];
"ExtremallyDisconnected" -> "TopologicalSpace" [style=dashed];
"PathConnectedSpace" -> "TopologicalSpace" [style=dashed];
"HasBesicovitchCovering" -> "MetricSpace" [style=dashed];
"PreirreducibleSpace" -> "TopologicalSpace" [style=dashed];
"TopologicalSpace.SeparableSpace" -> "TopologicalSpace" [style=dashed];
"FrechetUrysohnSpace" -> "TopologicalSpace" [style=dashed];
"IsReduced" -> "Pow" [style=dashed];
"IsReduced" -> "Zero" [style=dashed];
"CategoryTheory.LeftRigidCategory" -> "CategoryTheory.MonoidalCategory" [style=dashed];
"CategoryTheory.LeftRigidCategory" -> "CategoryTheory.Category" [style=dashed];
"IsWeakUpperModularLattice" -> "Lattice" [style=dashed];
"UniformAddGroup" -> "UniformSpace" [style=dashed];
"UniformAddGroup" -> "AddGroup" [style=dashed];
"Archimedean" -> "OrderedAddCommMonoid" [style=dashed];
"RightDistribClass" -> "Mul" [style=dashed];
"RightDistribClass" -> "Add" [style=dashed];
"CategoryTheory.IsFilteredOrEmpty" -> "CategoryTheory.Category" [style=dashed];
}
Raw
MessyCode.lean
import Mathlib
open Lean Meta Elab Command
-- generalized
/-- Write an import graph, represented as a an array of `NameMap`s to the ".dot" graph format.
If `("style1", graph1)` is in `graphs`, then the edges in `graph1` will be labeled with `[style1]`.
Example: `asStyledDotGraph #[("", graph1), ("style=dashed", graph2)]` -/
def asStyledDotGraph [ForIn Id α Name] (graphs : Array (String × NameMap α))
(header := "import_graph") : String := Id.run do
let mut lines := #[s!"digraph \"{header}\" " ++ "{"]
for (style, graph) in graphs do
let label := if style == "" then "" else s!" [{style}]"
for (n, is) in graph do
for i in is do
lines := lines.push s!" \"{n}\" -> \"{i}\"{label};"
lines := lines.push "}"
return "\n".intercalate lines.toList
/-- Write an import graph, represented as a a `NameMap` to the ".dot" graph format. -/
def asDotGraph [ForIn Id α Name] (graph : NameMap α) (header := "import_graph") : String :=
asStyledDotGraph #[("", graph)] header
-- slightly modified from elsewhere
private def isBlackListed (declName : Name) : CoreM Bool := do
if declName.getRoot == `Lean then return true
let env ← getEnv
pure $ declName.isInternal'
|| isAuxRecursor env declName
|| isNoConfusion env declName
<||> isRec declName <||> isMatcher declName
namespace Lean
instance (α : Type u) (cmp : α → α → Ordering) : Singleton α (RBTree α cmp) where
singleton x := .insert ∅ x
instance : Singleton Name NameSet where
singleton x := .insert ∅ x
instance (α : Type u) (cmp : α → α → Ordering) : Insert α (RBTree α cmp) where
insert x xs := xs.insert x
instance : Insert Name NameSet where
insert x xs := xs.insert x
/-- Given `t : RBMap α β` where the value type `β` implements `Singleton γ β` and `Insert γ β`
instances.
For example, `β = List γ` or `β = RBTree γ`. Then `t.insert2 x (y : γ)` inserts `y` at key `x` into
`t`. -/
def RBMap.insert2 [Singleton γ β] [Insert γ β] {cmp : α → α → Ordering} (t : RBMap α β cmp)
(x : α) (y : γ) : RBMap α β cmp :=
match t.find? x with
| some ys => t.insert x (Insert.insert y ys)
| none => t.insert x {y}
/-- `RBMap.insert2` specialized to `NameMap`. -/
def NameMap.insert2 [Singleton γ β] [Insert γ β] (t : NameMap β)
(x : Name) (y : γ) : NameMap β :=
RBMap.insert2 t x y
end Lean
/-- this instance causes a cycle -/
def blacklisted : NameSet :=
.ofList [`CategoryTheory.locallySmall_self]
#check NonemptyFinLinOrd.toFintype
/--
Retrieve all names in the environment satisfying a predicate as a NameSet.
-/
def allNamesAsSet (p : Name → Bool) : CoreM NameSet := do
(← getEnv).constants.foldM (init := {}) fun names n _ => do
if p n && !(← isBlackListed n) then
return names.insert n
else
return names
-- set_option profiler true
-- set_option trace.profiler true
def getClassInstanceGraph (full := true) : MetaM (NameMap NameSet) := do
let classes := classExtension.getState (← getEnv) |>.outParamMap.toList.map (·.1)
let classes : List (Name × List Name) ← classes.filterMapM fun nm => do
forallTelescope (← inferType (← mkConstWithLevelParams nm)) fun args _ => do
unless full || args.size == 1 do return none
let ldecls ← args.mapM (·.fvarId!.getDecl)
let bis := ldecls.map (·.binderInfo)
unless bis.toList.count .default == 1 && bis[0]? == some .default &&
ldecls[0]!.type.isSort do return none
let tgts := ldecls.toList.drop 1 |>.map (·.type.getAppFnArgs.1)
return some (nm, tgts)
let argumentGraph : NameMap NameSet := classes.foldl (init := {}) fun r (src, tgts) =>
r.insert src <| .ofList tgts
let classes : NameSet := .ofList <| classes.map (·.1)
let instances := instanceExtension.getState (← getEnv) |>.instanceNames.toList.map (·.1)
let instances : List (Name × List Name × Name) ← instances.filterMapM fun nm => do
forallTelescope (← inferType (← mkConstWithLevelParams nm)) fun args ty => do
unless args.size ≥ 2 do return none
unless full || args.size == 2 do return none
let typeVar := args[0]!
let (targetClass, targetClassArgs) := ty.getAppFnArgs
unless classes.contains targetClass do return none
unless targetClassArgs[0]? == some typeVar do return none
if blacklisted.contains nm then return none
let mut srcs := []
let mut dupes : NameSet := {}
for arg in args.toList.drop 1 do
let (sourceClass, sourceClassArgs) := (← inferType arg).getAppFnArgs
unless classes.contains sourceClass do return none
unless sourceClassArgs[0]? == some typeVar do return none
srcs := sourceClass::srcs
dupes := dupes ++ (argumentGraph.find? sourceClass).get!
let sources := srcs.filter (!dupes.contains ·)
return (nm, sources, targetClass)
let instanceGraph : NameMap NameSet := instances.foldl (init := {}) fun r (_, src, tgt) =>
if src.length == 1 then r.insert2 src.head! tgt else r
logInfo m!"classes with 1 type parameter: {classes.size}"
logInfo m!"instances between these classes: {instances.length}"
-- logInfo m!"classes: {classes}"
logInfo m!"forgetful instances with 1 source class: {instanceGraph.size}"
logInfo m!"argument instances: {argumentGraph.size}"
-- logInfo m!"instances: {instances}"
logInfo m!"{asStyledDotGraph #[("", instanceGraph), ("style=dashed", argumentGraph)] "instance_graph"}"
logInfo m!"instances with more than 1 source: {instances.filter (·.2.1.length > 1)}"
return instanceGraph
-- #check SemilinearEquivClass
set_option profiler true
run_cmd liftCoreM <| MetaM.run' <| do
getClassInstanceGraph
Raw
moreInstances.txt
instances with more than 1 source: [(LocallyFiniteOrder.toLocallyFiniteOrderTop,
([OrderTop, LocallyFiniteOrder], LocallyFiniteOrderTop)),
(invariantBasisNumber_of_nontrivial_of_commRing, ([Nontrivial, CommRing], InvariantBasisNumber)),
(LinearOrder.topologicalLattice, ([OrderClosedTopology, LinearOrder], TopologicalLattice)),
(ContinuousInf.measurableInf, ([ContinuousInf, BorelSpace], MeasurableInf)),
(isNilpotent_of_subsingleton, ([Subsingleton, Group], Group.IsNilpotent)),
(CategoryTheory.ProjectiveResolution.instHasProjectiveResolutionsHasZeroObjectPreadditiveHasZeroMorphismsToPreadditiveHasEqualizersHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisations,
([CategoryTheory.EnoughProjectives, CategoryTheory.Abelian], CategoryTheory.HasProjectiveResolutions)),
(CategoryTheory.isFiltered_of_semilatticeSup_nonempty, ([Nonempty, SemilatticeSup], CategoryTheory.IsFiltered)),
(OrderClosedTopology.to_t2Space, ([OrderClosedTopology, PartialOrder], T2Space)),
(DiscreteTopology.secondCountableTopology_of_encodable,
([Encodable, DiscreteTopology], TopologicalSpace.SecondCountableTopology)),
(ContinuousAdd.measurableAdd, ([ContinuousAdd, BorelSpace], MeasurableAdd)),
(LatticeOrderedCommGroup.hasZeroLatticeHasNegPart, ([AddCommGroup, Lattice], NegPart)),
(instNoTopOrderToLE, ([NoMaxOrder, Preorder], NoTopOrder)),
(LinearOrderedCommGroup.to_noMaxOrder, ([Nontrivial, LinearOrderedCommGroup], NoMaxOrder)),
(Group.existsMulOfLE, ([LE, Group], ExistsMulOfLE)),
(LinearOrder.supConvergenceClass, ([OrderTopology, LinearOrder], SupConvergenceClass)),
(baire_category_theorem_emetric_complete, ([CompleteSpace, PseudoEMetricSpace], BaireSpace)),
(LinearOrderedSemifield.toHasContinuousInv₀,
([ContinuousMul, OrderTopology, LinearOrderedSemifield], HasContinuousInv₀)),
(sigmaCompactSpace_of_locally_compact_second_countable,
([TopologicalSpace.SecondCountableTopology, LocallyCompactSpace], SigmaCompactSpace)),
(IsSimpleOrder.instIsAtomistic, ([IsSimpleOrder, CompleteLattice], IsAtomistic)),
(ContinuousMul.measurableMul, ([ContinuousMul, BorelSpace], MeasurableMul)),
(isReduced_of_noZeroDivisors, ([NoZeroDivisors, MonoidWithZero], IsReduced)),
(IsSimpleOrder.instIsCoatomicToPartialOrderToSemilatticeInfToOrderTopToLEToPreorder,
([IsSimpleOrder, Lattice], IsCoatomic)),
(LinearOrder.isPredArchimedean_of_isSuccArchimedean, ([IsSuccArchimedean, PredOrder, LinearOrder], IsPredArchimedean)),
(measurableDiv_of_mul_inv, ([MeasurableInv, MeasurableMul, DivInvMonoid], MeasurableDiv)),
(TopologicalSpace.Finite.to_noetherianSpace, ([Finite, TopologicalSpace], TopologicalSpace.NoetherianSpace)),
(Finite.to_isCoatomic, ([Finite, OrderTop, PartialOrder], IsCoatomic)),
(isSolvable_of_subsingleton, ([Subsingleton, Group], IsSolvable)),
(polish_of_countable, ([DiscreteTopology, Countable], PolishSpace)),
(SeparableLocallyCompactGroup.sigmaCompactSpace,
([LocallyCompactSpace, TopologicalSpace.SeparableSpace, TopologicalGroup], SigmaCompactSpace)),
(IsBezout.instIsIntegrallyClosed, ([IsBezout, IsDomain], IsIntegrallyClosed)),
(UniqueFactorizationMonoid.instIsIntegrallyClosed,
([UniqueFactorizationMonoid, IsDomain, CommRing], IsIntegrallyClosed)),
(ContinuousSup.measurableSup, ([ContinuousSup, BorelSpace], MeasurableSup)),
(LinearLocallyFiniteOrder.isSuccArchimedean, ([LocallyFiniteOrder, LinearOrder], IsSuccArchimedean)),
(CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot,
([OrderBot, SemilatticeSup], CategoryTheory.Limits.HasFiniteColimits)),
(IsSimpleOrder.instIsAtomicToPartialOrderToSemilatticeInfToOrderBotToLEToPreorder,
([IsSimpleOrder, Lattice], IsAtomic)),
(LinearOrderedField.toTopologicalDivisionRing, ([OrderTopology, LinearOrderedField], TopologicalDivisionRing)),
(SlimCheck.Testable.decidableTestable, ([Decidable, SlimCheck.PrintableProp], SlimCheck.Testable)),
(Subsingleton.discreteTopology, ([Subsingleton, TopologicalSpace], DiscreteTopology)),
(LowerTopology.continuousInf, ([LowerTopology, CompleteLattice], ContinuousInf)),
(MulZeroClass.negZeroClass, ([HasDistribNeg, MulZeroClass], NegZeroClass)),
(UpperTopology.continuousInf, ([UpperTopology, CompleteLattice], ContinuousSup)),
(polishSpace_of_complete_second_countable,
([CompleteSpace, TopologicalSpace.SecondCountableTopology, MetricSpace], PolishSpace)),
(completableTopField_of_complete,
([CompleteSpace, SeparatedSpace, TopologicalDivisionRing, Field], CompletableTopField)),
(CategoryTheory.isCofiltered_of_semilatticeInf_nonempty, ([Nonempty, SemilatticeInf], CategoryTheory.IsCofiltered)),
(ContinuousMul.measurableMul₂,
([ContinuousMul, TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableMul₂)),
(Subsingleton.compactSpace, ([Subsingleton, TopologicalSpace], CompactSpace)),
(Monoid.fg_of_finite, ([Finite, Monoid], Monoid.FG)),
(baire_category_theorem_locally_compact, ([LocallyCompactSpace, T2Space], BaireSpace)),
(compactSpace_of_completeLinearOrder, ([OrderTopology, CompleteLinearOrder], CompactSpace)),
(CategoryTheory.InjectiveResolution.instHasInjectiveResolutionsHasZeroObjectPreadditiveHasZeroMorphismsToPreadditiveHasEqualizersHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisations,
([CategoryTheory.EnoughInjectives, CategoryTheory.Abelian], CategoryTheory.HasInjectiveResolutions)),
(paracompact_of_locallyCompact_sigmaCompact, ([T2Space, SigmaCompactSpace, LocallyCompactSpace], ParacompactSpace)),
(DiscreteTopology.orderTopology_of_pred_succ, ([SuccOrder, PredOrder, LinearOrder, DiscreteTopology], OrderTopology)),
(FloorRing.archimedean, ([FloorRing, LinearOrderedField], Archimedean)),
(ordered_connected_space, ([DenselyOrdered, OrderTopology, ConditionallyCompleteLinearOrder], PreconnectedSpace)),
(Lean.Server.instRpcEncodable, ([Lean.ToJson, Lean.FromJson], Lean.Server.RpcEncodable)),
(isAddCyclic_of_subsingleton, ([Subsingleton, AddGroup], IsAddCyclic)),
(IsDomain.to_noZeroDivisors, ([IsDomain, Ring], NoZeroDivisors)),
(locally_compact_of_compact, ([CompactSpace, T2Space], LocallyCompactSpace)),
(IsSimpleAddGroup.isAddCyclic, ([IsSimpleAddGroup, AddCommGroup], IsAddCyclic)),
(DiscreteTopology.secondCountableTopology_of_countable,
([Countable, DiscreteTopology], TopologicalSpace.SecondCountableTopology)),
(OrderTopology.to_orderClosedTopology, ([OrderTopology, LinearOrder], OrderClosedTopology)),
(CstarRing.instNormOneClassToNormToOneToSemiringToRing, ([Nontrivial, CstarRing, NormedRing], NormOneClass)),
(AddMonoid.fg_of_finite, ([Finite, AddMonoid], AddMonoid.FG)),
(OrderTopology.t5Space, ([OrderTopology, LinearOrder], T5Space)),
(commRing_strongRankCondition, ([Nontrivial, CommRing], StrongRankCondition)),
(CanonicallyOrderedAddMonoid.toZeroLeOneClass, ([One, CanonicallyOrderedAddMonoid], ZeroLEOneClass)),
(TopologicalAddGroup.measurableNeg, ([TopologicalAddGroup, BorelSpace], MeasurableNeg)),
(measurableDiv₂_of_add_neg, ([MeasurableNeg, MeasurableAdd₂, SubNegMonoid], MeasurableSub₂)),
(AddGroup.fg_of_finite, ([Finite, AddGroup], AddGroup.FG)),
(Inv.toHasAbs, ([Sup, Inv], Abs)),
(HasContinuousInv₀.measurableInv, ([HasContinuousInv₀, T1Space, GroupWithZero, BorelSpace], MeasurableInv)),
(StarOrderedRing.toOrderedAddCommGroup, ([StarOrderedRing, NonUnitalRing], OrderedAddCommGroup)),
(IsBezout.of_isPrincipalIdealRing, ([IsPrincipalIdealRing, CommRing], IsBezout)),
(FirstCountableTopology.seq_compact_of_compact,
([CompactSpace, TopologicalSpace.FirstCountableTopology], SeqCompactSpace)),
(ContinuousSup.measurableSup₂,
([ContinuousSup, TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableSup₂)),
(PrincipalIdealRing.to_uniqueFactorizationMonoid,
([IsPrincipalIdealRing, IsDomain, CommRing], UniqueFactorizationMonoid)),
(LinearOrderedCommGroup.to_noMinOrder, ([Nontrivial, LinearOrderedCommGroup], NoMinOrder)),
(instNoBotOrderToLE, ([NoMinOrder, Preorder], NoBotOrder)),
(DiscreteTopology.orderTopology_of_pred_succ',
([NoMaxOrder, NoMinOrder, SuccOrder, PredOrder, PartialOrder, DiscreteTopology], OrderTopology)),
(DiscreteTopology.topologicalSemiring, ([DiscreteTopology, NonUnitalNonAssocSemiring], TopologicalSemiring)),
(LinearOrderedField.topologicalRing, ([OrderTopology, LinearOrderedField], TopologicalRing)),
(TopologicalGroup.measurableInv, ([TopologicalGroup, BorelSpace], MeasurableInv)),
(IsPrincipalIdealRing.isDedekindDomain, ([IsPrincipalIdealRing, IsDomain, CommRing], IsDedekindDomain)),
(UpperTopology.t0Space, ([UpperTopology, PartialOrder], T0Space)),
(BorelSpace.countablyGenerated,
([TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableSpace.CountablyGenerated)),
(proper_of_compact, ([CompactSpace, PseudoMetricSpace], ProperSpace)),
(ContinuousAdd.measurableMul₂,
([ContinuousAdd, TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableAdd₂)),
(LowerTopology.t0Space, ([LowerTopology, PartialOrder], T0Space)),
(IsSimpleGroup.isCyclic, ([IsSimpleGroup, CommGroup], IsCyclic)),
(continuousMul_of_discreteTopology, ([DiscreteTopology, Mul], ContinuousMul)),
(ContinuousSub.measurableSub₂,
([ContinuousSub, TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableSub₂)),
(GCDMonoid.toIsIntegrallyClosed, ([GCDMonoid, IsDomain, CommRing], IsIntegrallyClosed)),
(ConditionallyCompleteLinearOrder.toCompactIccSpace,
([OrderTopology, ConditionallyCompleteLinearOrder], CompactIccSpace)),
(TopologicalSpace.Countable.to_separableSpace, ([Countable, TopologicalSpace], TopologicalSpace.SeparableSpace)),
(OpensMeasurableSpace.toMeasurableSingletonClass, ([T1Space, OpensMeasurableSpace], MeasurableSingletonClass)),
(SeparableLocallyCompactAddGroup.sigmaCompactSpace,
([LocallyCompactSpace, TopologicalSpace.SeparableSpace, TopologicalAddGroup], SigmaCompactSpace)),
(complete_of_compact, ([CompactSpace, UniformSpace], CompleteSpace)),
(isAtomistic_of_complementedLattice, ([ComplementedLattice, IsCompactlyGenerated, IsModularLattice], IsAtomistic)),
(LatticeOrderedCommGroup.hasOneLatticeHasPosPart, ([CommGroup, Lattice], PosPart)),
(CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop,
([OrderTop, SemilatticeInf], CategoryTheory.Limits.HasFiniteLimits)),
(continuousAdd_of_discreteTopology, ([DiscreteTopology, Add], ContinuousAdd)),
(measurableDiv₂_of_mul_inv, ([MeasurableInv, MeasurableMul₂, DivInvMonoid], MeasurableDiv₂)),
(LatticeOrderedCommGroup.hasZeroLatticeHasPosPart, ([AddCommGroup, Lattice], PosPart)),
(countable_of_linear_succ_pred_arch, ([IsSuccArchimedean, PredOrder, LinearOrder], Countable)),
(AddGroup.existsAddOfLE, ([LE, AddGroup], ExistsAddOfLE)),
(IsSimpleOrder.instIsCoatomistic, ([IsSimpleOrder, CompleteLattice], IsCoatomistic)),
(measurableSub_of_add_neg, ([MeasurableNeg, MeasurableAdd, SubNegMonoid], MeasurableSub)),
(continuousInv_of_discreteTopology, ([DiscreteTopology, Inv], ContinuousInv)),
(NoZeroDivisors.to_isCancelMulZero, ([NoZeroDivisors, Ring], IsCancelMulZero)),
(LinearOrderedAddCommGroup.topologicalAddGroup, ([OrderTopology, LinearOrderedAddCommGroup], TopologicalAddGroup)),
(LinearOrderedAddCommGroup.to_noMinOrder, ([Nontrivial, LinearOrderedAddCommGroup], NoMinOrder)),
(PriestleySpace.toT2Space, ([PriestleySpace, PartialOrder], T2Space)),
(isCyclic_of_subsingleton, ([Subsingleton, Group], IsCyclic)),
(LinearOrderedAddCommGroup.to_noMaxOrder, ([Nontrivial, LinearOrderedAddCommGroup], NoMaxOrder)),
(Finite.compactSpace, ([Finite, TopologicalSpace], CompactSpace)),
(continuousNeg_of_discreteTopology, ([DiscreteTopology, Neg], ContinuousNeg)),
(LinearOrder.infConvergenceClass, ([OrderTopology, LinearOrder], InfConvergenceClass)),
(Finite.to_isAtomic, ([Finite, OrderBot, PartialOrder], IsAtomic)),
(IsDomain.toCancelCommMonoidWithZero, ([IsDomain, CommSemiring], CancelCommMonoidWithZero)),
(DiscreteTopology.topologicalRing, ([DiscreteTopology, NonUnitalNonAssocRing], TopologicalRing)),
(ContinuousInf.measurableInf₂,
([ContinuousInf, TopologicalSpace.SecondCountableTopology, BorelSpace], MeasurableInf₂)),
(Group.fg_of_finite, ([Finite, Group], Group.FG)),
(Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot, ([LocallyFiniteOrder, OrderBot], LocallyFiniteOrderBot)),
(ContinuousSub.measurableSub, ([ContinuousSub, BorelSpace], MeasurableSub)),
(Ring.DimensionLEOne.principal_ideal_ring, ([IsPrincipalIdealRing, IsDomain, CommRing], Ring.DimensionLEOne)),
(Neg.toHasAbs, ([Sup, Neg], Abs)),
(LinearLocallyFiniteOrder.instPredOrderToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice,
([LocallyFiniteOrder, LinearOrder], PredOrder)),
(LinearLocallyFiniteOrder.instSuccOrderToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice,
([LocallyFiniteOrder, LinearOrder], SuccOrder)),
(isAtomic_of_complementedLattice, ([ComplementedLattice, IsCompactlyGenerated, IsModularLattice], IsAtomic)),
(LatticeOrderedCommGroup.hasOneLatticeHasNegPart, ([CommGroup, Lattice], NegPart))]
Raw
partial.dot
digraph "instance_graph" {
"ConditionallyCompleteLinearOrderedField" -> "InfSet";
"ConditionallyCompleteLinearOrderedField" -> "SupSet";
"ConditionallyCompleteLinearOrderedField" -> "Sup";
"ConditionallyCompleteLinearOrderedField" -> "ConditionallyCompleteLinearOrder";
"ConditionallyCompleteLinearOrderedField" -> "Inf";
"ConditionallyCompleteLinearOrderedField" -> "LinearOrderedField";
"BiheytingAlgebra" -> "CoheytingAlgebra";
"BiheytingAlgebra" -> "HNot";
"BiheytingAlgebra" -> "SDiff";
"BiheytingAlgebra" -> "HeytingAlgebra";
"UpgradedPolishSpace" -> "MetricSpace";
"Nontrivial" -> "Nonempty";
"Semigroup" -> "Dvd";
"Semigroup" -> "Mul";
"CanonicallyLinearOrderedSemifield" -> "Nontrivial";
"CanonicallyLinearOrderedSemifield" -> "Inv";
"CanonicallyLinearOrderedSemifield" -> "Ord";
"CanonicallyLinearOrderedSemifield" -> "Max";
"CanonicallyLinearOrderedSemifield" -> "Div";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedCommGroupWithZero";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedSemifield";
"CanonicallyLinearOrderedSemifield" -> "Min";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyLinearOrderedAddMonoid";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyOrderedCommSemiring";
"StrictOrderedCommRing" -> "CommRing";
"StrictOrderedCommRing" -> "OrderedCommRing";
"StrictOrderedCommRing" -> "StrictOrderedRing";
"StrictOrderedCommRing" -> "StrictOrderedCommSemiring";
"OrderedCommGroup" -> "PartialOrder";
"OrderedCommGroup" -> "CommGroup";
"OrderedCommGroup" -> "OrderedCancelCommMonoid";
"Monoid" -> "Semigroup";
"Monoid" -> "One";
"Monoid" -> "MulOneClass";
"UniformSpace" -> "TopologicalSpace";
"NonUnitalNonAssocRing" -> "Mul";
"NonUnitalNonAssocRing" -> "AddCommGroup";
"NonUnitalNonAssocRing" -> "NonUnitalNonAssocSemiring";
"LinearOrderedCancelAddCommMonoid" -> "Ord";
"LinearOrderedCancelAddCommMonoid" -> "Max";
"LinearOrderedCancelAddCommMonoid" -> "LinearOrderedAddCommMonoid";
"LinearOrderedCancelAddCommMonoid" -> "Min";
"LinearOrderedCancelAddCommMonoid" -> "OrderedCancelAddCommMonoid";
"SemigroupWithZero" -> "Semigroup";
"SemigroupWithZero" -> "MulZeroClass";
"SemigroupWithZero" -> "Zero";
"Lattice" -> "SemilatticeInf";
"Lattice" -> "SemilatticeSup";
"Lattice" -> "Inf";
"BooleanAlgebra" -> "BiheytingAlgebra";
"BooleanAlgebra" -> "HImp";
"BooleanAlgebra" -> "HasCompl";
"BooleanAlgebra" -> "Bot";
"BooleanAlgebra" -> "DistribLattice";
"BooleanAlgebra" -> "GeneralizedBooleanAlgebra";
"BooleanAlgebra" -> "SDiff";
"BooleanAlgebra" -> "Top";
"OrderedCommMonoid" -> "PartialOrder";
"OrderedCommMonoid" -> "CommMonoid";
"NonUnitalSeminormedRing" -> "SeminormedAddCommGroup";
"NonUnitalSeminormedRing" -> "Norm";
"NonUnitalSeminormedRing" -> "PseudoMetricSpace";
"NonUnitalSeminormedRing" -> "NonUnitalRing";
"OrderedAddCommMonoid" -> "PartialOrder";
"OrderedAddCommMonoid" -> "AddCommMonoid";
"CompleteSemilatticeSup" -> "PartialOrder";
"CompleteSemilatticeSup" -> "SupSet";
"CommRing" -> "AddCommGroupWithOne";
"CommRing" -> "NonUnitalCommRing";
"CommRing" -> "CommSemiring";
"CommRing" -> "CommMonoid";
"CommRing" -> "Ring";
"LinearOrderedAddCommGroupWithTop" -> "Nontrivial";
"LinearOrderedAddCommGroupWithTop" -> "SubNegMonoid";
"LinearOrderedAddCommGroupWithTop" -> "Neg";
"LinearOrderedAddCommGroupWithTop" -> "LinearOrderedAddCommMonoidWithTop";
"LinearOrderedAddCommGroupWithTop" -> "Sub";
"StrictOrderedSemiring" -> "Nontrivial";
"StrictOrderedSemiring" -> "PartialOrder";
"StrictOrderedSemiring" -> "OrderedSemiring";
"StrictOrderedSemiring" -> "OrderedCancelAddCommMonoid";
"StrictOrderedSemiring" -> "Semiring";
"AddCommGroupWithOne" -> "One";
"AddCommGroupWithOne" -> "IntCast";
"AddCommGroupWithOne" -> "AddCommMonoidWithOne";
"AddCommGroupWithOne" -> "AddCommGroup";
"AddCommGroupWithOne" -> "NatCast";
"AddCommGroupWithOne" -> "AddGroupWithOne";
"One" -> "Nonempty";
"SeminormedAddCommGroup" -> "SeminormedAddGroup";
"SeminormedAddCommGroup" -> "AddCommGroup";
"SeminormedAddCommGroup" -> "Norm";
"SeminormedAddCommGroup" -> "PseudoMetricSpace";
"AddLeftCancelSemigroup" -> "AddSemigroup";
"LinearOrderedCommGroup" -> "OrderedCommGroup";
"LinearOrderedCommGroup" -> "Ord";
"LinearOrderedCommGroup" -> "LinearOrder";
"LinearOrderedCommGroup" -> "Max";
"LinearOrderedCommGroup" -> "LinearOrderedCancelCommMonoid";
"LinearOrderedCommGroup" -> "Min";
"AddCancelCommMonoid" -> "AddLeftCancelMonoid";
"AddCancelCommMonoid" -> "AddCancelMonoid";
"AddCancelCommMonoid" -> "AddCommMonoid";
"NormedCommRing" -> "SeminormedCommRing";
"NormedCommRing" -> "NormedRing";
"SeminormedCommRing" -> "CommRing";
"SeminormedCommRing" -> "SeminormedRing";
"KleeneAlgebra" -> "KStar";
"KleeneAlgebra" -> "IdemSemiring";
"Quandle" -> "Rack";
"OrderedRing" -> "PartialOrder";
"OrderedRing" -> "OrderedSemiring";
"OrderedRing" -> "OrderedAddCommGroup";
"OrderedRing" -> "Ring";
"LinearOrderedCommSemiring" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedCommSemiring" -> "Ord";
"LinearOrderedCommSemiring" -> "Max";
"LinearOrderedCommSemiring" -> "Min";
"LinearOrderedCommSemiring" -> "StrictOrderedCommSemiring";
"LinearOrderedCommSemiring" -> "LinearOrderedSemiring";
"NormedGroup" -> "SeminormedGroup";
"NormedGroup" -> "Group";
"NormedGroup" -> "Norm";
"NormedGroup" -> "MetricSpace";
"LinearOrder" -> "Lattice";
"LinearOrder" -> "Ord";
"LinearOrder" -> "Max";
"LinearOrder" -> "PartialOrder";
"LinearOrder" -> "Min";
"LinearOrder" -> "DistribLattice";
"SeminormedGroup" -> "Group";
"SeminormedGroup" -> "NNNorm";
"SeminormedGroup" -> "Norm";
"SeminormedGroup" -> "PseudoMetricSpace";
"Finite" -> "Countable";
"Unique" -> "Fintype";
"Unique" -> "Inhabited";
"Unique" -> "Subsingleton";
"ConditionallyCompleteLinearOrderBot" -> "Bot";
"ConditionallyCompleteLinearOrderBot" -> "ConditionallyCompleteLinearOrder";
"InvolutiveStar" -> "Star";
"CancelCommMonoidWithZero" -> "CommMonoidWithZero";
"CancelCommMonoidWithZero" -> "CancelMonoidWithZero";
"SeminormedAddGroup" -> "NNNorm";
"SeminormedAddGroup" -> "Norm";
"SeminormedAddGroup" -> "PseudoMetricSpace";
"SeminormedAddGroup" -> "AddGroup";
"DivisionCommMonoid" -> "DivisionMonoid";
"DivisionCommMonoid" -> "CommMonoid";
"GroupWithZero" -> "Nontrivial";
"GroupWithZero" -> "Inv";
"GroupWithZero" -> "DivisionMonoid";
"GroupWithZero" -> "Div";
"GroupWithZero" -> "DivInvMonoid";
"GroupWithZero" -> "MonoidWithZero";
"GroupWithZero" -> "CancelMonoidWithZero";
"Rack" -> "Shelf";
"CompleteAtomicBooleanAlgebra" -> "HImp";
"CompleteAtomicBooleanAlgebra" -> "CompletelyDistribLattice";
"CompleteAtomicBooleanAlgebra" -> "CompleteBooleanAlgebra";
"CompleteAtomicBooleanAlgebra" -> "HasCompl";
"CompleteAtomicBooleanAlgebra" -> "SDiff";
"NormedLatticeAddCommGroup" -> "Lattice";
"NormedLatticeAddCommGroup" -> "OrderedAddCommGroup";
"NormedLatticeAddCommGroup" -> "NormedAddCommGroup";
"ConditionallyCompleteLattice" -> "Lattice";
"ConditionallyCompleteLattice" -> "InfSet";
"ConditionallyCompleteLattice" -> "SupSet";
"GeneralizedCoheytingAlgebra" -> "Lattice";
"GeneralizedCoheytingAlgebra" -> "Bot";
"GeneralizedCoheytingAlgebra" -> "DistribLattice";
"GeneralizedCoheytingAlgebra" -> "SDiff";
"Group" -> "DivisionMonoid";
"Group" -> "DivInvMonoid";
"Group" -> "CancelMonoid";
"CompleteDistribLattice" -> "Order.Coframe";
"CompleteDistribLattice" -> "Order.Frame";
"SubNegMonoid" -> "Neg";
"SubNegMonoid" -> "AddMonoid";
"SubNegMonoid" -> "Sub";
"DivInvOneMonoid" -> "DivInvMonoid";
"DivInvOneMonoid" -> "InvOneClass";
"AddLeftCancelMonoid" -> "AddLeftCancelSemigroup";
"AddLeftCancelMonoid" -> "AddMonoid";
"AddLeftCancelMonoid" -> "Zero";
"AddCommMonoidWithOne" -> "AddCommMonoid";
"AddCommMonoidWithOne" -> "AddMonoidWithOne";
"MulZeroClass" -> "Mul";
"MulZeroClass" -> "Zero";
"LinearOrderedRing" -> "Ord";
"LinearOrderedRing" -> "LinearOrder";
"LinearOrderedRing" -> "Max";
"LinearOrderedRing" -> "Min";
"LinearOrderedRing" -> "LinearOrderedAddCommGroup";
"LinearOrderedRing" -> "StrictOrderedRing";
"LinearOrderedRing" -> "LinearOrderedSemiring";
"AddCancelMonoid" -> "AddLeftCancelMonoid";
"AddCancelMonoid" -> "AddRightCancelMonoid";
"PartialOrder" -> "Preorder";
"CategoryTheory.Groupoid" -> "CategoryTheory.Category";
"AddCommGroup" -> "AddCancelCommMonoid";
"AddCommGroup" -> "AddCommMonoid";
"AddCommGroup" -> "AddGroup";
"AddCommGroup" -> "SubtractionCommMonoid";
"DivisionMonoid" -> "DivInvOneMonoid";
"DivisionMonoid" -> "InvolutiveInv";
"DivisionMonoid" -> "DivInvMonoid";
"NormedLinearOrderedField" -> "Norm";
"NormedLinearOrderedField" -> "NormedField";
"NormedLinearOrderedField" -> "MetricSpace";
"NormedLinearOrderedField" -> "LinearOrderedField";
"InfSet" -> "Nonempty";
"OrderedSemiring" -> "OrderedAddCommMonoid";
"OrderedSemiring" -> "PartialOrder";
"OrderedSemiring" -> "Semiring";
"CoheytingAlgebra" -> "GeneralizedCoheytingAlgebra";
"CoheytingAlgebra" -> "DistribLattice";
"CoheytingAlgebra" -> "HNot";
"CoheytingAlgebra" -> "Top";
"Semifield" -> "Nontrivial";
"Semifield" -> "Inv";
"Semifield" -> "Div";
"Semifield" -> "CommSemiring";
"Semifield" -> "DivisionSemiring";
"Semifield" -> "CommGroupWithZero";
"CanonicallyOrderedMonoid" -> "OrderedCommMonoid";
"CanonicallyOrderedMonoid" -> "Bot";
"CompletelyDistribLattice" -> "CompleteDistribLattice";
"CompletelyDistribLattice" -> "CompleteLattice";
"CircularPreorder" -> "Btw";
"CircularPreorder" -> "SBtw";
"CompleteBooleanAlgebra" -> "BooleanAlgebra";
"CompleteBooleanAlgebra" -> "CompleteDistribLattice";
"CompleteBooleanAlgebra" -> "InfSet";
"CompleteBooleanAlgebra" -> "SupSet";
"Setoid" -> "HasEquiv";
"NonUnitalNormedRing" -> "NonUnitalSeminormedRing";
"NonUnitalNormedRing" -> "Norm";
"NonUnitalNormedRing" -> "MetricSpace";
"NonUnitalNormedRing" -> "NonUnitalRing";
"NonUnitalNormedRing" -> "NormedAddCommGroup";
"NonAssocRing" -> "NonUnitalNonAssocRing";
"NonAssocRing" -> "AddCommGroupWithOne";
"NonAssocRing" -> "One";
"NonAssocRing" -> "IntCast";
"NonAssocRing" -> "NatCast";
"NonAssocRing" -> "NonAssocSemiring";
"NonUnitalCommRing" -> "CommSemigroup";
"NonUnitalCommRing" -> "NonUnitalRing";
"NonUnitalCommRing" -> "NonUnitalCommSemiring";
"SupSet" -> "Nonempty";
"LinearOrderedAddCommMonoid" -> "OrderedAddCommMonoid";
"LinearOrderedAddCommMonoid" -> "LinearOrder";
"LinearOrderedAddCommMonoid" -> "AddCommMonoid";
"Bot" -> "Nonempty";
"MulZeroOneClass" -> "MulZeroClass";
"MulZeroOneClass" -> "MulOneClass";
"MulZeroOneClass" -> "Zero";
"CommGroup" -> "DivisionCommMonoid";
"CommGroup" -> "Group";
"CommGroup" -> "CommMonoid";
"CommGroup" -> "CancelCommMonoid";
"IsEmpty" -> "Fintype";
"IsEmpty" -> "Subsingleton";
"IsEmpty" -> "Encodable";
"Std.ToFormat" -> "Lean.ToMessageData";
"LinearOrderedCommGroupWithZero" -> "Nontrivial";
"LinearOrderedCommGroupWithZero" -> "Inv";
"LinearOrderedCommGroupWithZero" -> "Div";
"LinearOrderedCommGroupWithZero" -> "LinearOrderedCommMonoidWithZero";
"LinearOrderedCommGroupWithZero" -> "CommGroupWithZero";
"LinearOrderedCancelCommMonoid" -> "Ord";
"LinearOrderedCancelCommMonoid" -> "Max";
"LinearOrderedCancelCommMonoid" -> "Min";
"LinearOrderedCancelCommMonoid" -> "LinearOrderedCommMonoid";
"LinearOrderedCancelCommMonoid" -> "OrderedCancelCommMonoid";
"AddSemigroup" -> "Add";
"LinearOrderedSemifield" -> "Inv";
"LinearOrderedSemifield" -> "LinearOrderedCommSemiring";
"LinearOrderedSemifield" -> "Semifield";
"LinearOrderedSemifield" -> "Div";
"RightCancelMonoid" -> "Monoid";
"RightCancelMonoid" -> "One";
"RightCancelMonoid" -> "RightCancelSemigroup";
"OrderedCommRing" -> "CommRing";
"OrderedCommRing" -> "OrderedRing";
"OrderedCommRing" -> "OrderedCommSemiring";
"PseudoEMetricSpace" -> "UniformSpace";
"PseudoEMetricSpace" -> "EDist";
"InvolutiveInv" -> "Inv";
"EMetricSpace" -> "PseudoEMetricSpace";
"DivInvMonoid" -> "Monoid";
"DivInvMonoid" -> "Inv";
"DivInvMonoid" -> "Div";
"CircularPartialOrder" -> "CircularPreorder";
"NormedField" -> "NormedCommRing";
"NormedField" -> "Norm";
"NormedField" -> "MetricSpace";
"NormedField" -> "Field";
"NormedField" -> "NormedDivisionRing";
"InvOneClass" -> "One";
"InvOneClass" -> "Inv";
"LeftCancelSemigroup" -> "Semigroup";
"AddCommMonoid" -> "AddMonoid";
"AddCommMonoid" -> "AddCommSemigroup";
"Lean.Eval" -> "Lean.MetaEval";
"LinearOrderedCommRing" -> "StrictOrderedCommRing";
"LinearOrderedCommRing" -> "LinearOrderedCommSemiring";
"LinearOrderedCommRing" -> "LinearOrderedRing";
"LinearOrderedCommRing" -> "CommMonoid";
"NormedCommGroup" -> "NormedGroup";
"NormedCommGroup" -> "Norm";
"NormedCommGroup" -> "CommGroup";
"NormedCommGroup" -> "MetricSpace";
"NormedCommGroup" -> "SeminormedCommGroup";
"CommSemiring" -> "CommMonoidWithZero";
"CommSemiring" -> "Semiring";
"CommSemiring" -> "NonUnitalCommSemiring";
"CommSemiring" -> "CommMonoid";
"OmegaCompletePartialOrder" -> "PartialOrder";
"AddRightCancelMonoid" -> "AddRightCancelSemigroup";
"AddRightCancelMonoid" -> "AddMonoid";
"AddRightCancelMonoid" -> "Zero";
"CommSemigroup" -> "Semigroup";
"IdemCommSemiring" -> "CommSemiring";
"IdemCommSemiring" -> "IdemSemiring";
"IdemCommSemiring" -> "SemilatticeSup";
"DivisionSemiring" -> "Nontrivial";
"DivisionSemiring" -> "Inv";
"DivisionSemiring" -> "GroupWithZero";
"DivisionSemiring" -> "Div";
"DivisionSemiring" -> "Semiring";
"OrderedCommSemiring" -> "OrderedSemiring";
"OrderedCommSemiring" -> "CommSemiring";
"CategoryTheory.Bicategory" -> "CategoryTheory.CategoryStruct";
"DistribLattice" -> "Lattice";
"LieRing" -> "AddCommGroup";
"InvolutiveNeg" -> "Neg";
"PseudoMetricSpace" -> "UniformSpace";
"PseudoMetricSpace" -> "NNDist";
"PseudoMetricSpace" -> "PseudoEMetricSpace";
"PseudoMetricSpace" -> "Dist";
"PseudoMetricSpace" -> "EDist";
"PseudoMetricSpace" -> "Bornology";
"AddGroup" -> "SubNegMonoid";
"AddGroup" -> "AddCancelMonoid";
"AddGroup" -> "SubtractionMonoid";
"AddZeroClass" -> "Add";
"AddZeroClass" -> "Zero";
"SemilatticeInf" -> "PartialOrder";
"SemilatticeInf" -> "Inf";
"MonoidWithZero" -> "Monoid";
"MonoidWithZero" -> "SemigroupWithZero";
"MonoidWithZero" -> "MulZeroOneClass";
"MonoidWithZero" -> "Zero";
"LeftCancelMonoid" -> "Monoid";
"LeftCancelMonoid" -> "One";
"LeftCancelMonoid" -> "LeftCancelSemigroup";
"SubNegZeroMonoid" -> "SubNegMonoid";
"SubNegZeroMonoid" -> "NegZeroClass";
"NonAssocSemiring" -> "One";
"NonAssocSemiring" -> "AddCommMonoidWithOne";
"NonAssocSemiring" -> "NatCast";
"NonAssocSemiring" -> "MulZeroOneClass";
"NonAssocSemiring" -> "NonUnitalNonAssocSemiring";
"DenselyNormedField" -> "NormedField";
"DenselyNormedField" -> "NontriviallyNormedField";
"UnitalShelf" -> "One";
"UnitalShelf" -> "Shelf";
"Fintype" -> "Finite";
"Fintype" -> "Small";
"AddRightCancelSemigroup" -> "AddSemigroup";
"MetricSpace" -> "EMetricSpace";
"MetricSpace" -> "PseudoMetricSpace";
"Order.Coframe" -> "DistribLattice";
"Order.Coframe" -> "CompleteLattice";
"LinearOrderedAddCommMonoidWithTop" -> "LinearOrderedAddCommMonoid";
"LinearOrderedAddCommMonoidWithTop" -> "Top";
"SubtractionMonoid" -> "SubNegMonoid";
"SubtractionMonoid" -> "InvolutiveNeg";
"SubtractionMonoid" -> "SubNegZeroMonoid";
"LinearOrderedCommMonoidWithZero" -> "CommMonoidWithZero";
"LinearOrderedCommMonoidWithZero" -> "LinearOrderedCommMonoid";
"LinearOrderedCommMonoidWithZero" -> "Zero";
"NonUnitalSemiring" -> "SemigroupWithZero";
"NonUnitalSemiring" -> "NonUnitalNonAssocSemiring";
"CanonicallyOrderedAddMonoid" -> "OrderedAddCommMonoid";
"CanonicallyOrderedAddMonoid" -> "Bot";
"CanonicallyLinearOrderedAddMonoid" -> "Ord";
"CanonicallyLinearOrderedAddMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedAddMonoid" -> "Max";
"CanonicallyLinearOrderedAddMonoid" -> "Min";
"CanonicallyLinearOrderedAddMonoid" -> "CanonicallyOrderedAddMonoid";
"CanonicallyLinearOrderedAddMonoid" -> "SemilatticeSup";
"CommMonoidWithZero" -> "MonoidWithZero";
"CommMonoidWithZero" -> "CommMonoid";
"CommMonoidWithZero" -> "Zero";
"GeneralizedBooleanAlgebra" -> "GeneralizedCoheytingAlgebra";
"GeneralizedBooleanAlgebra" -> "Bot";
"GeneralizedBooleanAlgebra" -> "DistribLattice";
"GeneralizedBooleanAlgebra" -> "SDiff";
"EuclideanDomain" -> "Mod";
"EuclideanDomain" -> "Nontrivial";
"EuclideanDomain" -> "CommRing";
"EuclideanDomain" -> "Div";
"OrderedCancelAddCommMonoid" -> "OrderedAddCommMonoid";
"OrderedCancelAddCommMonoid" -> "AddCancelCommMonoid";
"OrderedCancelAddCommMonoid" -> "PartialOrder";
"OrderedCancelAddCommMonoid" -> "AddCommMonoid";
"Distrib" -> "Mul";
"Distrib" -> "Add";
"LinearOrderedAddCommGroup" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedAddCommGroup" -> "Ord";
"LinearOrderedAddCommGroup" -> "LinearOrder";
"LinearOrderedAddCommGroup" -> "Max";
"LinearOrderedAddCommGroup" -> "Min";
"LinearOrderedAddCommGroup" -> "OrderedAddCommGroup";
"CommGroupWithZero" -> "Nontrivial";
"CommGroupWithZero" -> "Inv";
"CommGroupWithZero" -> "CancelCommMonoidWithZero";
"CommGroupWithZero" -> "DivisionCommMonoid";
"CommGroupWithZero" -> "GroupWithZero";
"CommGroupWithZero" -> "Div";
"CommGroupWithZero" -> "CommMonoidWithZero";
"ToString" -> "Std.ToFormat";
"ToString" -> "Lean.Eval";
"AddMonoid" -> "AddSemigroup";
"AddMonoid" -> "AddZeroClass";
"AddMonoid" -> "Zero";
"NormedLinearOrderedAddGroup" -> "Norm";
"NormedLinearOrderedAddGroup" -> "MetricSpace";
"NormedLinearOrderedAddGroup" -> "LinearOrderedAddCommGroup";
"NormedLinearOrderedAddGroup" -> "NormedOrderedAddGroup";
"LinearOrderedCommMonoid" -> "OrderedCommMonoid";
"LinearOrderedCommMonoid" -> "LinearOrder";
"LinearOrderedCommMonoid" -> "CommMonoid";
"CancelMonoid" -> "RightCancelMonoid";
"CancelMonoid" -> "LeftCancelMonoid";
"Primcodable" -> "Encodable";
"Semiring" -> "One";
"Semiring" -> "NatCast";
"Semiring" -> "MonoidWithZero";
"Semiring" -> "NonAssocSemiring";
"Semiring" -> "NonUnitalSemiring";
"NontriviallyNormedField" -> "NormedField";
"Countable" -> "Small";
"CompleteLinearOrder" -> "LinearOrder";
"CompleteLinearOrder" -> "ConditionallyCompleteLinearOrderBot";
"CompleteLinearOrder" -> "CompletelyDistribLattice";
"CompleteLinearOrder" -> "CompleteLattice";
"Inhabited" -> "Nonempty";
"Subsingleton" -> "Finite";
"Subsingleton" -> "Countable";
"Subsingleton" -> "Small";
"FinEnum" -> "Fintype";
"CompleteSemilatticeInf" -> "PartialOrder";
"CompleteSemilatticeInf" -> "InfSet";
"AddGroupWithOne" -> "IntCast";
"AddGroupWithOne" -> "Neg";
"AddGroupWithOne" -> "AddGroup";
"AddGroupWithOne" -> "AddMonoidWithOne";
"AddGroupWithOne" -> "Sub";
"CategoryTheory.CategoryStruct" -> "Quiver";
"StrictOrderedRing" -> "Nontrivial";
"StrictOrderedRing" -> "StrictOrderedSemiring";
"StrictOrderedRing" -> "OrderedRing";
"StrictOrderedRing" -> "PartialOrder";
"StrictOrderedRing" -> "OrderedAddCommGroup";
"StrictOrderedRing" -> "Ring";
"DivisionRing" -> "Nontrivial";
"DivisionRing" -> "Inv";
"DivisionRing" -> "OfScientific";
"DivisionRing" -> "Div";
"DivisionRing" -> "DivInvMonoid";
"DivisionRing" -> "DivisionSemiring";
"DivisionRing" -> "RatCast";
"DivisionRing" -> "Ring";
"NormedOrderedAddGroup" -> "Norm";
"NormedOrderedAddGroup" -> "MetricSpace";
"NormedOrderedAddGroup" -> "OrderedAddCommGroup";
"NormedOrderedAddGroup" -> "NormedAddCommGroup";
"Infinite" -> "Nontrivial";
"SizeOf" -> "WellFoundedRelation";
"NormedOrderedGroup" -> "OrderedCommGroup";
"NormedOrderedGroup" -> "Norm";
"NormedOrderedGroup" -> "NormedCommGroup";
"NormedOrderedGroup" -> "MetricSpace";
"NonUnitalRing" -> "NonUnitalNonAssocRing";
"NonUnitalRing" -> "NonUnitalSemiring";
"NonUnitalCommSemiring" -> "CommSemigroup";
"NonUnitalCommSemiring" -> "NonUnitalSemiring";
"HeytingAlgebra" -> "HasCompl";
"HeytingAlgebra" -> "Bot";
"HeytingAlgebra" -> "GeneralizedHeytingAlgebra";
"NormedLinearOrderedGroup" -> "LinearOrderedCommGroup";
"NormedLinearOrderedGroup" -> "Norm";
"NormedLinearOrderedGroup" -> "MetricSpace";
"NormedLinearOrderedGroup" -> "NormedOrderedGroup";
"ConditionallyCompleteLinearOrder" -> "LinearOrder";
"ConditionallyCompleteLinearOrder" -> "ConditionallyCompleteLattice";
"Order.Frame" -> "DistribLattice";
"Order.Frame" -> "CompleteLattice";
"AddCommSemigroup" -> "AddSemigroup";
"SeminormedCommGroup" -> "SeminormedGroup";
"SeminormedCommGroup" -> "Norm";
"SeminormedCommGroup" -> "CommGroup";
"SeminormedCommGroup" -> "PseudoMetricSpace";
"MulOneClass" -> "One";
"MulOneClass" -> "Mul";
"SubtractionCommMonoid" -> "AddCommMonoid";
"SubtractionCommMonoid" -> "SubtractionMonoid";
"Denumerable" -> "Primcodable";
"Denumerable" -> "Infinite";
"Denumerable" -> "Encodable";
"RightCancelSemigroup" -> "Semigroup";
"NonUnitalNonAssocSemiring" -> "Mul";
"NonUnitalNonAssocSemiring" -> "MulZeroClass";
"NonUnitalNonAssocSemiring" -> "AddCommMonoid";
"NonUnitalNonAssocSemiring" -> "Distrib";
"NegZeroClass" -> "Neg";
"NegZeroClass" -> "Zero";
"OrderedAddCommGroup" -> "PartialOrder";
"OrderedAddCommGroup" -> "AddCommGroup";
"OrderedAddCommGroup" -> "OrderedCancelAddCommMonoid";
"StrictOrderedCommSemiring" -> "StrictOrderedSemiring";
"StrictOrderedCommSemiring" -> "CommSemiring";
"StrictOrderedCommSemiring" -> "OrderedCommSemiring";
"CompleteLattice" -> "Lattice";
"CompleteLattice" -> "CompleteSemilatticeSup";
"CompleteLattice" -> "ConditionallyCompleteLattice";
"CompleteLattice" -> "InfSet";
"CompleteLattice" -> "SupSet";
"CompleteLattice" -> "Bot";
"CompleteLattice" -> "OmegaCompletePartialOrder";
"CompleteLattice" -> "CompleteSemilatticeInf";
"CompleteLattice" -> "Top";
"Repr" -> "ReprTuple";
"Repr" -> "Lean.Eval";
"OrderedCancelCommMonoid" -> "OrderedCommMonoid";
"OrderedCancelCommMonoid" -> "PartialOrder";
"OrderedCancelCommMonoid" -> "CommMonoid";
"OrderedCancelCommMonoid" -> "CancelCommMonoid";
"LinearOrderedSemiring" -> "StrictOrderedSemiring";
"LinearOrderedSemiring" -> "Ord";
"LinearOrderedSemiring" -> "Max";
"LinearOrderedSemiring" -> "LinearOrderedAddCommMonoid";
"LinearOrderedSemiring" -> "Min";
"IdemSemiring" -> "CanonicallyOrderedAddMonoid";
"IdemSemiring" -> "Semiring";
"IdemSemiring" -> "SemilatticeSup";
"CommMonoid" -> "Monoid";
"CommMonoid" -> "CommSemigroup";
"SemilatticeSup" -> "PartialOrder";
"SemilatticeSup" -> "Sup";
"Field" -> "Nontrivial";
"Field" -> "CommRing";
"Field" -> "Inv";
"Field" -> "Semifield";
"Field" -> "Div";
"Field" -> "RatCast";
"Field" -> "EuclideanDomain";
"Field" -> "DivisionRing";
"Ring" -> "IntCast";
"Ring" -> "AddCommGroup";
"Ring" -> "NonAssocRing";
"Ring" -> "LieRing";
"Ring" -> "Neg";
"Ring" -> "Semiring";
"Ring" -> "AddGroupWithOne";
"Ring" -> "NonUnitalRing";
"Ring" -> "Sub";
"GeneralizedHeytingAlgebra" -> "Lattice";
"GeneralizedHeytingAlgebra" -> "HImp";
"GeneralizedHeytingAlgebra" -> "DistribLattice";
"GeneralizedHeytingAlgebra" -> "Top";
"MeasureTheory.MeasureSpace" -> "MeasurableSpace";
"NormedRing" -> "Norm";
"NormedRing" -> "NonUnitalNormedRing";
"NormedRing" -> "MetricSpace";
"NormedRing" -> "Ring";
"NormedRing" -> "SeminormedRing";
"NonemptyFinLinOrd" -> "LinearOrder";
"NonemptyFinLinOrd" -> "Fintype";
"NonemptyFinLinOrd" -> "Nonempty";
"CanonicallyOrderedCommSemiring" -> "OrderedCommMonoid";
"CanonicallyOrderedCommSemiring" -> "One";
"CanonicallyOrderedCommSemiring" -> "Mul";
"CanonicallyOrderedCommSemiring" -> "NatCast";
"CanonicallyOrderedCommSemiring" -> "CommSemiring";
"CanonicallyOrderedCommSemiring" -> "OrderedCommSemiring";
"CanonicallyOrderedCommSemiring" -> "CanonicallyOrderedAddMonoid";
"Top" -> "Nonempty";
"SeminormedRing" -> "NonUnitalSeminormedRing";
"SeminormedRing" -> "Norm";
"SeminormedRing" -> "PseudoMetricSpace";
"SeminormedRing" -> "Ring";
"NormedDivisionRing" -> "Norm";
"NormedDivisionRing" -> "MetricSpace";
"NormedDivisionRing" -> "DivisionRing";
"NormedDivisionRing" -> "NormedRing";
"CancelMonoidWithZero" -> "MonoidWithZero";
"LinearOrderedField" -> "Inv";
"LinearOrderedField" -> "Div";
"LinearOrderedField" -> "LinearOrderedSemifield";
"LinearOrderedField" -> "LinearOrderedCommRing";
"LinearOrderedField" -> "RatCast";
"LinearOrderedField" -> "Field";
"Encodable" -> "Countable";
"CircularOrder" -> "CircularPartialOrder";
"Preorder" -> "LE";
"Preorder" -> "LT";
"BooleanRing" -> "CommRing";
"BooleanRing" -> "Ring";
"NormedAddCommGroup" -> "SeminormedAddCommGroup";
"NormedAddCommGroup" -> "AddCommGroup";
"NormedAddCommGroup" -> "Norm";
"NormedAddCommGroup" -> "MetricSpace";
"NormedAddCommGroup" -> "NormedAddGroup";
"AddMonoidWithOne" -> "One";
"AddMonoidWithOne" -> "NatCast";
"AddMonoidWithOne" -> "AddMonoid";
"CategoryTheory.Category" -> "CategoryTheory.CategoryStruct";
"CanonicallyLinearOrderedMonoid" -> "Ord";
"CanonicallyLinearOrderedMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedMonoid" -> "Max";
"CanonicallyLinearOrderedMonoid" -> "CanonicallyOrderedMonoid";
"CanonicallyLinearOrderedMonoid" -> "Min";
"CanonicallyLinearOrderedMonoid" -> "SemilatticeSup";
"NormedAddGroup" -> "SeminormedAddGroup";
"NormedAddGroup" -> "Norm";
"NormedAddGroup" -> "AddGroup";
"NormedAddGroup" -> "MetricSpace";
"CancelCommMonoid" -> "LeftCancelMonoid";
"CancelCommMonoid" -> "CancelMonoid";
"CancelCommMonoid" -> "CommMonoid";
"Zero" -> "Nonempty";
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment