From a2c9da6c3998d7f53aae3b25642950c2cba97957 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 09:37:50 -0500 Subject: [PATCH 1/9] feat: port CategoryTheory.IsomorphismClasses From 7fb21a3fcb4ff4cfb5f6597e30c3f5b07b606893 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 09:37:50 -0500 Subject: [PATCH 2/9] Initial file copy from mathport --- .../CategoryTheory/IsomorphismClasses.lean | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 Mathlib/CategoryTheory/IsomorphismClasses.lean diff --git a/Mathlib/CategoryTheory/IsomorphismClasses.lean b/Mathlib/CategoryTheory/IsomorphismClasses.lean new file mode 100644 index 0000000000000..e612f2ee34e7e --- /dev/null +++ b/Mathlib/CategoryTheory/IsomorphismClasses.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2019 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov + +! This file was ported from Lean 3 source module category_theory.isomorphism_classes +! leanprover-community/mathlib commit 28aa996fc6fb4317f0083c4e6daf79878d81be33 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.CategoryTheory.Category.Cat +import Mathbin.CategoryTheory.Groupoid +import Mathbin.CategoryTheory.Types + +/-! +# Objects of a category up to an isomorphism + +`is_isomorphic X Y := nonempty (X ≅ Y)` is an equivalence relation on the objects of a category. +The quotient with respect to this relation defines a functor from our category to `Type`. +-/ + + +universe v u + +namespace CategoryTheory + +section Category + +variable {C : Type u} [Category.{v} C] + +/-- An object `X` is isomorphic to an object `Y`, if `X ≅ Y` is not empty. -/ +def IsIsomorphic : C → C → Prop := fun X Y => Nonempty (X ≅ Y) +#align category_theory.is_isomorphic CategoryTheory.IsIsomorphic + +variable (C) + +/-- `is_isomorphic` defines a setoid. -/ +def isIsomorphicSetoid : Setoid C where + R := IsIsomorphic + iseqv := ⟨fun X => ⟨Iso.refl X⟩, fun X Y ⟨α⟩ => ⟨α.symm⟩, fun X Y Z ⟨α⟩ ⟨β⟩ => ⟨α.trans β⟩⟩ +#align category_theory.is_isomorphic_setoid CategoryTheory.isIsomorphicSetoid + +end Category + +/-- The functor that sends each category to the quotient space of its objects up to an isomorphism. +-/ +def isomorphismClasses : Cat.{v, u} ⥤ Type u + where + obj C := Quotient (isIsomorphicSetoid C.α) + map C D F := Quot.map F.obj fun X Y ⟨f⟩ => ⟨F.mapIso f⟩ +#align category_theory.isomorphism_classes CategoryTheory.isomorphismClasses + +theorem Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X Y : C} : + IsIsomorphic X Y ↔ Nonempty (X ⟶ Y) := + (Groupoid.isoEquivHom X Y).nonempty_congr +#align category_theory.groupoid.is_isomorphic_iff_nonempty_hom CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom + +-- PROJECT: define `skeletal`, and show every category is equivalent to a skeletal category, +-- using the axiom of choice to pick a representative of every isomorphism class. +end CategoryTheory + From f6f3b75cdb0805953f94585390ab728582b0272a Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 09:37:50 -0500 Subject: [PATCH 3/9] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/CategoryTheory/IsomorphismClasses.lean | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index ed492c90e4606..17b2d323831e5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -250,6 +250,7 @@ import Mathlib.CategoryTheory.Functor.InvIsos import Mathlib.CategoryTheory.Groupoid import Mathlib.CategoryTheory.Groupoid.Basic import Mathlib.CategoryTheory.Iso +import Mathlib.CategoryTheory.IsomorphismClasses import Mathlib.CategoryTheory.Monoidal.Category import Mathlib.CategoryTheory.NatIso import Mathlib.CategoryTheory.NatTrans diff --git a/Mathlib/CategoryTheory/IsomorphismClasses.lean b/Mathlib/CategoryTheory/IsomorphismClasses.lean index e612f2ee34e7e..54b851141ac5f 100644 --- a/Mathlib/CategoryTheory/IsomorphismClasses.lean +++ b/Mathlib/CategoryTheory/IsomorphismClasses.lean @@ -8,9 +8,9 @@ Authors: Yury Kudryashov ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.CategoryTheory.Category.Cat -import Mathbin.CategoryTheory.Groupoid -import Mathbin.CategoryTheory.Types +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Groupoid +import Mathlib.CategoryTheory.Types /-! # Objects of a category up to an isomorphism From a388072fee3db25d8da58423cf31f6a1367f355f Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 09:40:16 -0500 Subject: [PATCH 4/9] :wqaSquashed commit of the following: commit 8f688834c49993c79921e0afc71fa9ccbb76c2ad Merge: 405cecc8 eab0a098 Author: Matthew Ballard Date: Mon Feb 20 09:37:07 2023 -0500 Merge branch 'master' into port/CategoryTheory.Category.Cat commit 405cecc8a84ba71400c2c62111bb2f4af345d911 Author: Matthew Ballard Date: Sun Feb 19 08:48:18 2023 -0500 fix errors; lint commit 25b73831798574ad738915a65319211df3bb00ce Author: Matthew Ballard Date: Sun Feb 19 08:11:21 2023 -0500 remove script commit dfa581d0f0c88b68f62b5276404409cec48057d1 Author: Matthew Ballard Date: Sun Feb 19 08:10:44 2023 -0500 Squashed commit of the following: commit 24c70cbb23f140fc451716c7d346ac4c19888da6 Merge: 38a89b87 18f8822c Author: Matthew Ballard Date: Thu Feb 16 20:20:59 2023 -0500 Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.DiscreteCategory' into port/CategoryTheory.DiscreteCategory commit 38a89b87e6655d9e89c6b89032e22096d94d24b5 Author: Matthew Ballard Date: Thu Feb 16 20:20:24 2023 -0500 lint some more commit 18f8822c79724d281f17886fd67d55461d5a867e Merge: eb146446 68e722a8 Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> Date: Thu Feb 16 20:16:53 2023 -0500 Merge branch 'master' into port/CategoryTheory.DiscreteCategory commit eb1464469358a6a9502a0b8ddaba399068e45293 Author: Matthew Ballard Date: Thu Feb 16 20:14:21 2023 -0500 lint commit 8860e0dbee2c5b58a3e890ba3447af0443052316 Author: adamtopaz Date: Thu Feb 16 17:33:00 2023 -0700 get file to build commit 22034856ebc97b161fcc7b9d476049ebeeb8daca Author: adamtopaz Date: Tue Feb 14 22:06:54 2023 -0700 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit 10bf4bb690318c385e5fa84948e4d987ad115bd9 Author: adamtopaz Date: Tue Feb 14 22:06:54 2023 -0700 Initial file copy from mathport commit 82e25124b8f38e2494e781bf4c1fd0ab432effc0 Author: adamtopaz Date: Tue Feb 14 22:06:54 2023 -0700 feat: port CategoryTheory.DiscreteCategory commit 64556c5cdbdcf14cc9fbdba3ee969df186a92c66 Author: Matthew Ballard Date: Sun Feb 19 08:08:19 2023 -0500 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit e14a0f5dd1306c8c397175601b946a3f4df6ee83 Author: Matthew Ballard Date: Sun Feb 19 08:08:19 2023 -0500 Initial file copy from mathport commit 967e14a61dc35153f4e5c563c799c1bd81d10c0e Author: Matthew Ballard Date: Sun Feb 19 08:08:19 2023 -0500 feat: port CategoryTheory.Category.Cat --- Mathlib.lean | 2 + Mathlib.lean.orig | 1197 ++++++++++++++++++ Mathlib/CategoryTheory/Category/Cat.lean | 178 +++ Mathlib/CategoryTheory/DiscreteCategory.lean | 364 ++++++ 4 files changed, 1741 insertions(+) create mode 100644 Mathlib.lean.orig create mode 100644 Mathlib/CategoryTheory/Category/Cat.lean create mode 100644 Mathlib/CategoryTheory/DiscreteCategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index 17b2d323831e5..70c113f8041e1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -225,6 +225,7 @@ import Mathlib.CategoryTheory.Balanced import Mathlib.CategoryTheory.Bicategory.Basic import Mathlib.CategoryTheory.Bicategory.Strict import Mathlib.CategoryTheory.Category.Basic +import Mathlib.CategoryTheory.Category.Cat import Mathlib.CategoryTheory.Category.KleisliCat import Mathlib.CategoryTheory.Category.Preorder import Mathlib.CategoryTheory.Category.RelCat @@ -232,6 +233,7 @@ import Mathlib.CategoryTheory.Comma import Mathlib.CategoryTheory.ConcreteCategory.Bundled import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Core +import Mathlib.CategoryTheory.DiscreteCategory import Mathlib.CategoryTheory.Endomorphism import Mathlib.CategoryTheory.EpiMono import Mathlib.CategoryTheory.EqToHom diff --git a/Mathlib.lean.orig b/Mathlib.lean.orig new file mode 100644 index 0000000000000..b65b902d4a6d0 --- /dev/null +++ b/Mathlib.lean.orig @@ -0,0 +1,1197 @@ +import Mathlib.Algebra.Abs +import Mathlib.Algebra.AddTorsor +import Mathlib.Algebra.Algebra.Basic +import Mathlib.Algebra.Associated +import Mathlib.Algebra.BigOperators.Associated +import Mathlib.Algebra.BigOperators.Basic +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.BigOperators.Finprod +import Mathlib.Algebra.BigOperators.Finsupp +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.BigOperators.Multiset.Basic +import Mathlib.Algebra.BigOperators.Multiset.Lemmas +import Mathlib.Algebra.BigOperators.NatAntidiagonal +import Mathlib.Algebra.BigOperators.Option +import Mathlib.Algebra.BigOperators.Order +import Mathlib.Algebra.BigOperators.Pi +import Mathlib.Algebra.BigOperators.Ring +import Mathlib.Algebra.BigOperators.RingEquiv +import Mathlib.Algebra.Bounds +import Mathlib.Algebra.CharZero.Defs +import Mathlib.Algebra.CharZero.Infinite +import Mathlib.Algebra.CharZero.Lemmas +import Mathlib.Algebra.CharZero.Quotient +import Mathlib.Algebra.CovariantAndContravariant +import Mathlib.Algebra.DirectSum.Basic +import Mathlib.Algebra.Divisibility.Basic +import Mathlib.Algebra.Divisibility.Units +import Mathlib.Algebra.EuclideanDomain.Basic +import Mathlib.Algebra.EuclideanDomain.Defs +import Mathlib.Algebra.EuclideanDomain.Instances +import Mathlib.Algebra.Field.Basic +import Mathlib.Algebra.Field.Defs +import Mathlib.Algebra.Field.Opposite +import Mathlib.Algebra.Field.Power +import Mathlib.Algebra.Free +import Mathlib.Algebra.FreeMonoid.Basic +import Mathlib.Algebra.FreeMonoid.Count +import Mathlib.Algebra.GCDMonoid.Basic +import Mathlib.Algebra.GCDMonoid.Finset +import Mathlib.Algebra.GCDMonoid.Multiset +import Mathlib.Algebra.GeomSum +import Mathlib.Algebra.GradedMonoid +import Mathlib.Algebra.GradedMulAction +import Mathlib.Algebra.Group.Basic +import Mathlib.Algebra.Group.Commutator +import Mathlib.Algebra.Group.Commute +import Mathlib.Algebra.Group.Conj +import Mathlib.Algebra.Group.ConjFinite +import Mathlib.Algebra.Group.Defs +import Mathlib.Algebra.Group.Ext +import Mathlib.Algebra.Group.InjSurj +import Mathlib.Algebra.Group.Opposite +import Mathlib.Algebra.Group.OrderSynonym +import Mathlib.Algebra.Group.Pi +import Mathlib.Algebra.Group.Prod +import Mathlib.Algebra.Group.Semiconj +import Mathlib.Algebra.Group.TypeTags +import Mathlib.Algebra.Group.ULift +import Mathlib.Algebra.Group.UniqueProds +import Mathlib.Algebra.Group.Units +import Mathlib.Algebra.Group.WithOne.Basic +import Mathlib.Algebra.Group.WithOne.Defs +import Mathlib.Algebra.Group.WithOne.Units +import Mathlib.Algebra.GroupPower.Basic +import Mathlib.Algebra.GroupPower.Identities +import Mathlib.Algebra.GroupPower.Lemmas +import Mathlib.Algebra.GroupPower.Order +import Mathlib.Algebra.GroupPower.Ring +import Mathlib.Algebra.GroupRingAction.Basic +import Mathlib.Algebra.GroupRingAction.Subobjects +import Mathlib.Algebra.GroupWithZero.Basic +import Mathlib.Algebra.GroupWithZero.Commute +import Mathlib.Algebra.GroupWithZero.Defs +import Mathlib.Algebra.GroupWithZero.Divisibility +import Mathlib.Algebra.GroupWithZero.InjSurj +import Mathlib.Algebra.GroupWithZero.Power +import Mathlib.Algebra.GroupWithZero.Semiconj +import Mathlib.Algebra.GroupWithZero.Units.Basic +import Mathlib.Algebra.GroupWithZero.Units.Lemmas +import Mathlib.Algebra.HierarchyDesign +import Mathlib.Algebra.Hom.Aut +import Mathlib.Algebra.Hom.Centroid +import Mathlib.Algebra.Hom.Commute +import Mathlib.Algebra.Hom.Embedding +import Mathlib.Algebra.Hom.Equiv.Basic +import Mathlib.Algebra.Hom.Equiv.TypeTags +import Mathlib.Algebra.Hom.Equiv.Units.Basic +import Mathlib.Algebra.Hom.Equiv.Units.GroupWithZero +import Mathlib.Algebra.Hom.Freiman +import Mathlib.Algebra.Hom.Group +import Mathlib.Algebra.Hom.GroupAction +import Mathlib.Algebra.Hom.GroupInstances +import Mathlib.Algebra.Hom.Iterate +import Mathlib.Algebra.Hom.Ring +import Mathlib.Algebra.Hom.Units +import Mathlib.Algebra.Homology.ComplexShape +import Mathlib.Algebra.IndicatorFunction +import Mathlib.Algebra.Invertible +import Mathlib.Algebra.IsPrimePow +import Mathlib.Algebra.Module.Basic +import Mathlib.Algebra.Module.BigOperators +import Mathlib.Algebra.Module.Equiv +import Mathlib.Algebra.Module.Hom +import Mathlib.Algebra.Module.LinearMap +import Mathlib.Algebra.Module.Opposites +import Mathlib.Algebra.Module.Pi +import Mathlib.Algebra.Module.PointwisePi +import Mathlib.Algebra.Module.Prod +import Mathlib.Algebra.Module.Submodule.Basic +import Mathlib.Algebra.Module.Submodule.Lattice +import Mathlib.Algebra.Module.Submodule.Pointwise +import Mathlib.Algebra.Module.ULift +import Mathlib.Algebra.NeZero +import Mathlib.Algebra.Opposites +import Mathlib.Algebra.Order.AbsoluteValue +import Mathlib.Algebra.Order.Archimedean +import Mathlib.Algebra.Order.EuclideanAbsoluteValue +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Algebra.Order.Field.Canonical.Basic +import Mathlib.Algebra.Order.Field.Canonical.Defs +import Mathlib.Algebra.Order.Field.Defs +import Mathlib.Algebra.Order.Field.InjSurj +import Mathlib.Algebra.Order.Field.Pi +import Mathlib.Algebra.Order.Field.Power +import Mathlib.Algebra.Order.Floor +import Mathlib.Algebra.Order.Group.Abs +import Mathlib.Algebra.Order.Group.Bounds +import Mathlib.Algebra.Order.Group.Defs +import Mathlib.Algebra.Order.Group.DenselyOrdered +import Mathlib.Algebra.Order.Group.InjSurj +import Mathlib.Algebra.Order.Group.Instances +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Algebra.Order.Group.OrderIso +import Mathlib.Algebra.Order.Group.Prod +import Mathlib.Algebra.Order.Group.TypeTags +import Mathlib.Algebra.Order.Group.Units +import Mathlib.Algebra.Order.Group.WithTop +import Mathlib.Algebra.Order.Hom.Basic +import Mathlib.Algebra.Order.Hom.Monoid +import Mathlib.Algebra.Order.Invertible +import Mathlib.Algebra.Order.Kleene +import Mathlib.Algebra.Order.LatticeGroup +import Mathlib.Algebra.Order.Module +import Mathlib.Algebra.Order.Monoid.Basic +import Mathlib.Algebra.Order.Monoid.Cancel.Basic +import Mathlib.Algebra.Order.Monoid.Cancel.Defs +import Mathlib.Algebra.Order.Monoid.Canonical.Defs +import Mathlib.Algebra.Order.Monoid.Defs +import Mathlib.Algebra.Order.Monoid.Lemmas +import Mathlib.Algebra.Order.Monoid.MinMax +import Mathlib.Algebra.Order.Monoid.NatCast +import Mathlib.Algebra.Order.Monoid.OrderDual +import Mathlib.Algebra.Order.Monoid.Prod +import Mathlib.Algebra.Order.Monoid.ToMulBot +import Mathlib.Algebra.Order.Monoid.TypeTags +import Mathlib.Algebra.Order.Monoid.Units +import Mathlib.Algebra.Order.Monoid.WithTop +import Mathlib.Algebra.Order.Monoid.WithZero.Basic +import Mathlib.Algebra.Order.Monoid.WithZero.Defs +import Mathlib.Algebra.Order.Nonneg.Field +import Mathlib.Algebra.Order.Nonneg.Ring +import Mathlib.Algebra.Order.Pi +import Mathlib.Algebra.Order.Pointwise +import Mathlib.Algebra.Order.Positive.Field +import Mathlib.Algebra.Order.Positive.Ring +import Mathlib.Algebra.Order.Ring.Abs +import Mathlib.Algebra.Order.Ring.Canonical +import Mathlib.Algebra.Order.Ring.CharZero +import Mathlib.Algebra.Order.Ring.Cone +import Mathlib.Algebra.Order.Ring.Defs +import Mathlib.Algebra.Order.Ring.InjSurj +import Mathlib.Algebra.Order.Ring.Lemmas +import Mathlib.Algebra.Order.Ring.WithTop +import Mathlib.Algebra.Order.SMul +import Mathlib.Algebra.Order.Sub.Basic +import Mathlib.Algebra.Order.Sub.Canonical +import Mathlib.Algebra.Order.Sub.Defs +import Mathlib.Algebra.Order.Sub.WithTop +import Mathlib.Algebra.Order.UpperLower +import Mathlib.Algebra.Order.WithZero +import Mathlib.Algebra.Order.ZeroLEOne +import Mathlib.Algebra.PEmptyInstances +import Mathlib.Algebra.PUnitInstances +import Mathlib.Algebra.Parity +import Mathlib.Algebra.Periodic +import Mathlib.Algebra.Quandle +import Mathlib.Algebra.Quotient +import Mathlib.Algebra.Regular.Basic +import Mathlib.Algebra.Regular.Pow +import Mathlib.Algebra.Regular.SMul +import Mathlib.Algebra.Ring.AddAut +import Mathlib.Algebra.Ring.Aut +import Mathlib.Algebra.Ring.Basic +import Mathlib.Algebra.Ring.Commute +import Mathlib.Algebra.Ring.CompTypeclasses +import Mathlib.Algebra.Ring.Defs +import Mathlib.Algebra.Ring.Divisibility +import Mathlib.Algebra.Ring.Equiv +import Mathlib.Algebra.Ring.Fin +import Mathlib.Algebra.Ring.Idempotents +import Mathlib.Algebra.Ring.InjSurj +import Mathlib.Algebra.Ring.Opposite +import Mathlib.Algebra.Ring.OrderSynonym +import Mathlib.Algebra.Ring.Pi +import Mathlib.Algebra.Ring.Prod +import Mathlib.Algebra.Ring.Regular +import Mathlib.Algebra.Ring.Semiconj +import Mathlib.Algebra.Ring.ULift +import Mathlib.Algebra.Ring.Units +import Mathlib.Algebra.SMulWithZero +import Mathlib.Algebra.Star.Basic +import Mathlib.Algebra.Star.BigOperators +import Mathlib.Algebra.Star.Pi +import Mathlib.Algebra.Star.Pointwise +import Mathlib.Algebra.Star.Prod +import Mathlib.Algebra.Star.SelfAdjoint +import Mathlib.Algebra.Star.Unitary +import Mathlib.Algebra.Support +import Mathlib.Algebra.Tropical.Basic +import Mathlib.Algebra.Tropical.BigOperators +import Mathlib.Algebra.Tropical.Lattice +import Mathlib.CategoryTheory.Arrow +import Mathlib.CategoryTheory.Balanced +import Mathlib.CategoryTheory.Bicategory.Basic +import Mathlib.CategoryTheory.Bicategory.Strict +import Mathlib.CategoryTheory.Category.Basic +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Category.KleisliCat +import Mathlib.CategoryTheory.Category.Preorder +import Mathlib.CategoryTheory.Category.RelCat +import Mathlib.CategoryTheory.Comma +import Mathlib.CategoryTheory.ConcreteCategory.Bundled +<<<<<<< HEAD +import Mathlib.CategoryTheory.Conj +import Mathlib.CategoryTheory.Core +======= +import Mathlib.CategoryTheory.DiscreteCategory +>>>>>>> port/CategoryTheory.DiscreteCategory +import Mathlib.CategoryTheory.Endomorphism +import Mathlib.CategoryTheory.EpiMono +import Mathlib.CategoryTheory.EqToHom +import Mathlib.CategoryTheory.Equivalence +import Mathlib.CategoryTheory.EssentialImage +import Mathlib.CategoryTheory.FullSubcategory +import Mathlib.CategoryTheory.Functor.Basic +import Mathlib.CategoryTheory.Functor.Category +import Mathlib.CategoryTheory.Functor.Const +import Mathlib.CategoryTheory.Functor.Currying +import Mathlib.CategoryTheory.Functor.Default +import Mathlib.CategoryTheory.Functor.FullyFaithful +import Mathlib.CategoryTheory.Functor.Functorial +import Mathlib.CategoryTheory.Functor.Hom +import Mathlib.CategoryTheory.Functor.InvIsos +import Mathlib.CategoryTheory.Groupoid +import Mathlib.CategoryTheory.Groupoid.Basic +import Mathlib.CategoryTheory.Iso +import Mathlib.CategoryTheory.Monoidal.Category +import Mathlib.CategoryTheory.NatIso +import Mathlib.CategoryTheory.NatTrans +import Mathlib.CategoryTheory.Opposites +import Mathlib.CategoryTheory.Pi.Basic +import Mathlib.CategoryTheory.Products.Associator +import Mathlib.CategoryTheory.Products.Basic +import Mathlib.CategoryTheory.Products.Bifunctor +import Mathlib.CategoryTheory.Sigma.Basic +import Mathlib.CategoryTheory.Thin +import Mathlib.CategoryTheory.Types +import Mathlib.CategoryTheory.Whiskering +import Mathlib.Combinatorics.Additive.Energy +import Mathlib.Combinatorics.Additive.RuzsaCovering +import Mathlib.Combinatorics.Colex +import Mathlib.Combinatorics.Composition +import Mathlib.Combinatorics.DoubleCounting +import Mathlib.Combinatorics.Hall.Finite +import Mathlib.Combinatorics.Partition +import Mathlib.Combinatorics.Pigeonhole +import Mathlib.Combinatorics.Quiver.Arborescence +import Mathlib.Combinatorics.Quiver.Basic +import Mathlib.Combinatorics.Quiver.Cast +import Mathlib.Combinatorics.Quiver.ConnectedComponent +import Mathlib.Combinatorics.Quiver.Path +import Mathlib.Combinatorics.Quiver.Push +import Mathlib.Combinatorics.Quiver.SingleObj +import Mathlib.Combinatorics.Quiver.Subquiver +import Mathlib.Combinatorics.Quiver.Symmetric +import Mathlib.Combinatorics.SetFamily.Compression.Down +import Mathlib.Combinatorics.SetFamily.Compression.UV +import Mathlib.Combinatorics.SetFamily.HarrisKleitman +import Mathlib.Combinatorics.SetFamily.Intersecting +import Mathlib.Combinatorics.SetFamily.Kleitman +import Mathlib.Combinatorics.SetFamily.LYM +import Mathlib.Combinatorics.SetFamily.Shadow +import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise +import Mathlib.Combinatorics.Young.SemistandardTableau +import Mathlib.Combinatorics.Young.YoungDiagram +import Mathlib.Computability.DFA +import Mathlib.Computability.Language +import Mathlib.Computability.NFA +import Mathlib.Computability.TuringMachine +import Mathlib.Control.Applicative +import Mathlib.Control.Basic +import Mathlib.Control.EquivFunctor +import Mathlib.Control.EquivFunctor.Instances +import Mathlib.Control.Fix +import Mathlib.Control.Functor +import Mathlib.Control.Functor.Multivariate +import Mathlib.Control.Monad.Basic +import Mathlib.Control.Random +import Mathlib.Control.SimpSet +import Mathlib.Control.Traversable.Basic +import Mathlib.Control.Traversable.Equiv +import Mathlib.Control.Traversable.Instances +import Mathlib.Control.Traversable.Lemmas +import Mathlib.Control.ULift +import Mathlib.Control.Writer +import Mathlib.Data.Analysis.Filter +import Mathlib.Data.Array.Basic +import Mathlib.Data.Array.Defs +import Mathlib.Data.BinaryHeap +import Mathlib.Data.Bitvec.Core +import Mathlib.Data.Bool.AllAny +import Mathlib.Data.Bool.Basic +import Mathlib.Data.Bool.Count +import Mathlib.Data.Bool.Set +import Mathlib.Data.Bracket +import Mathlib.Data.Bundle +import Mathlib.Data.ByteArray +import Mathlib.Data.Char +import Mathlib.Data.Countable.Basic +import Mathlib.Data.Countable.Defs +import Mathlib.Data.Countable.Small +import Mathlib.Data.DList.Basic +import Mathlib.Data.DList.Instances +import Mathlib.Data.Dfinsupp.Basic +import Mathlib.Data.Dfinsupp.Interval +import Mathlib.Data.Dfinsupp.Lex +import Mathlib.Data.Dfinsupp.Multiset +import Mathlib.Data.Dfinsupp.NeLocus +import Mathlib.Data.Dfinsupp.Order +import Mathlib.Data.ENat.Basic +import Mathlib.Data.ENat.Lattice +import Mathlib.Data.Equiv.Functor +import Mathlib.Data.Erased +import Mathlib.Data.FP.Basic +import Mathlib.Data.Fin.Basic +import Mathlib.Data.Fin.Fin2 +import Mathlib.Data.Fin.Interval +import Mathlib.Data.Fin.SuccPred +import Mathlib.Data.Fin.Tuple.Basic +import Mathlib.Data.Fin.Tuple.BubbleSortInduction +import Mathlib.Data.Fin.Tuple.Monotone +import Mathlib.Data.Fin.Tuple.NatAntidiagonal +import Mathlib.Data.Fin.Tuple.Sort +import Mathlib.Data.Fin.VecNotation +import Mathlib.Data.FinEnum +import Mathlib.Data.Finite.Basic +import Mathlib.Data.Finite.Card +import Mathlib.Data.Finite.Defs +import Mathlib.Data.Finite.Set +import Mathlib.Data.Finmap +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.Card +import Mathlib.Data.Finset.Fin +import Mathlib.Data.Finset.Finsupp +import Mathlib.Data.Finset.Fold +import Mathlib.Data.Finset.Functor +import Mathlib.Data.Finset.Image +import Mathlib.Data.Finset.Lattice +import Mathlib.Data.Finset.LocallyFinite +import Mathlib.Data.Finset.MulAntidiagonal +import Mathlib.Data.Finset.NAry +import Mathlib.Data.Finset.NatAntidiagonal +import Mathlib.Data.Finset.NoncommProd +import Mathlib.Data.Finset.Option +import Mathlib.Data.Finset.Order +import Mathlib.Data.Finset.PImage +import Mathlib.Data.Finset.Pairwise +import Mathlib.Data.Finset.Pi +import Mathlib.Data.Finset.PiInduction +import Mathlib.Data.Finset.Pointwise +import Mathlib.Data.Finset.Powerset +import Mathlib.Data.Finset.Preimage +import Mathlib.Data.Finset.Prod +import Mathlib.Data.Finset.Sigma +import Mathlib.Data.Finset.Slice +import Mathlib.Data.Finset.Sort +import Mathlib.Data.Finset.Sum +import Mathlib.Data.Finsupp.AList +import Mathlib.Data.Finsupp.Antidiagonal +import Mathlib.Data.Finsupp.Basic +import Mathlib.Data.Finsupp.BigOperators +import Mathlib.Data.Finsupp.Defs +import Mathlib.Data.Finsupp.Fin +import Mathlib.Data.Finsupp.Fintype +import Mathlib.Data.Finsupp.Indicator +import Mathlib.Data.Finsupp.Interval +import Mathlib.Data.Finsupp.Lex +import Mathlib.Data.Finsupp.Multiset +import Mathlib.Data.Finsupp.NeLocus +import Mathlib.Data.Finsupp.Order +import Mathlib.Data.Finsupp.Pointwise +import Mathlib.Data.Finsupp.Pwo +import Mathlib.Data.Finsupp.ToDfinsupp +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.Fintype.BigOperators +import Mathlib.Data.Fintype.Card +import Mathlib.Data.Fintype.CardEmbedding +import Mathlib.Data.Fintype.Fin +import Mathlib.Data.Fintype.Lattice +import Mathlib.Data.Fintype.List +import Mathlib.Data.Fintype.Option +import Mathlib.Data.Fintype.Order +import Mathlib.Data.Fintype.Parity +import Mathlib.Data.Fintype.Perm +import Mathlib.Data.Fintype.Pi +import Mathlib.Data.Fintype.Powerset +import Mathlib.Data.Fintype.Prod +import Mathlib.Data.Fintype.Sigma +import Mathlib.Data.Fintype.Small +import Mathlib.Data.Fintype.Sort +import Mathlib.Data.Fintype.Sum +import Mathlib.Data.Fintype.Units +import Mathlib.Data.Fintype.Vector +import Mathlib.Data.FunLike.Basic +import Mathlib.Data.FunLike.Embedding +import Mathlib.Data.FunLike.Equiv +import Mathlib.Data.FunLike.Fintype +import Mathlib.Data.HashMap +import Mathlib.Data.Holor +import Mathlib.Data.Int.AbsoluteValue +import Mathlib.Data.Int.Associated +import Mathlib.Data.Int.Basic +import Mathlib.Data.Int.Bitwise +import Mathlib.Data.Int.Cast.Basic +import Mathlib.Data.Int.Cast.Defs +import Mathlib.Data.Int.Cast.Field +import Mathlib.Data.Int.Cast.Lemmas +import Mathlib.Data.Int.Cast.Prod +import Mathlib.Data.Int.CharZero +import Mathlib.Data.Int.ConditionallyCompleteOrder +import Mathlib.Data.Int.Div +import Mathlib.Data.Int.Dvd.Basic +import Mathlib.Data.Int.Dvd.Pow +import Mathlib.Data.Int.GCD +import Mathlib.Data.Int.Interval +import Mathlib.Data.Int.LeastGreatest +import Mathlib.Data.Int.Lemmas +import Mathlib.Data.Int.Log +import Mathlib.Data.Int.ModEq +import Mathlib.Data.Int.NatPrime +import Mathlib.Data.Int.Order.Basic +import Mathlib.Data.Int.Order.Lemmas +import Mathlib.Data.Int.Order.Units +import Mathlib.Data.Int.Parity +import Mathlib.Data.Int.Range +import Mathlib.Data.Int.Sqrt +import Mathlib.Data.Int.SuccPred +import Mathlib.Data.Int.Units +import Mathlib.Data.KVMap +import Mathlib.Data.LazyList +import Mathlib.Data.LazyList.Basic +import Mathlib.Data.List.AList +import Mathlib.Data.List.Basic +import Mathlib.Data.List.BigOperators.Basic +import Mathlib.Data.List.BigOperators.Lemmas +import Mathlib.Data.List.Card +import Mathlib.Data.List.Chain +import Mathlib.Data.List.Count +import Mathlib.Data.List.Cycle +import Mathlib.Data.List.Dedup +import Mathlib.Data.List.Defs +import Mathlib.Data.List.Destutter +import Mathlib.Data.List.Duplicate +import Mathlib.Data.List.FinRange +import Mathlib.Data.List.Forall2 +import Mathlib.Data.List.Func +import Mathlib.Data.List.Indexes +import Mathlib.Data.List.Infix +import Mathlib.Data.List.Join +import Mathlib.Data.List.Lattice +import Mathlib.Data.List.Lemmas +import Mathlib.Data.List.Lex +import Mathlib.Data.List.MinMax +import Mathlib.Data.List.NatAntidiagonal +import Mathlib.Data.List.Nodup +import Mathlib.Data.List.NodupEquivFin +import Mathlib.Data.List.OfFn +import Mathlib.Data.List.Pairwise +import Mathlib.Data.List.Palindrome +import Mathlib.Data.List.Perm +import Mathlib.Data.List.Permutation +import Mathlib.Data.List.Prime +import Mathlib.Data.List.ProdSigma +import Mathlib.Data.List.Range +import Mathlib.Data.List.Rdrop +import Mathlib.Data.List.Rotate +import Mathlib.Data.List.Sections +import Mathlib.Data.List.Sigma +import Mathlib.Data.List.Sort +import Mathlib.Data.List.Sublists +import Mathlib.Data.List.TFAE +import Mathlib.Data.List.Zip +import Mathlib.Data.Matrix.DMatrix +import Mathlib.Data.Multiset.Antidiagonal +import Mathlib.Data.Multiset.Basic +import Mathlib.Data.Multiset.Bind +import Mathlib.Data.Multiset.Dedup +import Mathlib.Data.Multiset.FinsetOps +import Mathlib.Data.Multiset.Fintype +import Mathlib.Data.Multiset.Fold +import Mathlib.Data.Multiset.Functor +import Mathlib.Data.Multiset.Lattice +import Mathlib.Data.Multiset.LocallyFinite +import Mathlib.Data.Multiset.NatAntidiagonal +import Mathlib.Data.Multiset.Nodup +import Mathlib.Data.Multiset.Pi +import Mathlib.Data.Multiset.Powerset +import Mathlib.Data.Multiset.Range +import Mathlib.Data.Multiset.Sections +import Mathlib.Data.Multiset.Sort +import Mathlib.Data.Multiset.Sum +import Mathlib.Data.Nat.Basic +import Mathlib.Data.Nat.Bits +import Mathlib.Data.Nat.Bitwise +import Mathlib.Data.Nat.Cast.Basic +import Mathlib.Data.Nat.Cast.Defs +import Mathlib.Data.Nat.Cast.Field +import Mathlib.Data.Nat.Cast.Prod +import Mathlib.Data.Nat.Cast.WithTop +import Mathlib.Data.Nat.Choose.Basic +import Mathlib.Data.Nat.Choose.Bounds +import Mathlib.Data.Nat.Choose.Central +import Mathlib.Data.Nat.Choose.Dvd +import Mathlib.Data.Nat.Choose.Sum +import Mathlib.Data.Nat.Count +import Mathlib.Data.Nat.Dist +import Mathlib.Data.Nat.EvenOddRec +import Mathlib.Data.Nat.Factorial.Basic +import Mathlib.Data.Nat.Factorial.BigOperators +import Mathlib.Data.Nat.Factors +import Mathlib.Data.Nat.Fib +import Mathlib.Data.Nat.ForSqrt +import Mathlib.Data.Nat.GCD.Basic +import Mathlib.Data.Nat.GCD.BigOperators +import Mathlib.Data.Nat.Hyperoperation +import Mathlib.Data.Nat.Interval +import Mathlib.Data.Nat.Lattice +import Mathlib.Data.Nat.Log +import Mathlib.Data.Nat.ModEq +import Mathlib.Data.Nat.Order.Basic +import Mathlib.Data.Nat.Order.Lemmas +import Mathlib.Data.Nat.PSub +import Mathlib.Data.Nat.Pairing +import Mathlib.Data.Nat.Parity +import Mathlib.Data.Nat.PartENat +import Mathlib.Data.Nat.Periodic +import Mathlib.Data.Nat.Pow +import Mathlib.Data.Nat.Prime +import Mathlib.Data.Nat.PrimeFin +import Mathlib.Data.Nat.Set +import Mathlib.Data.Nat.Size +import Mathlib.Data.Nat.Sqrt +import Mathlib.Data.Nat.SuccPred +import Mathlib.Data.Nat.Units +import Mathlib.Data.Nat.Upto +import Mathlib.Data.Nat.WithBot +import Mathlib.Data.Num.Basic +import Mathlib.Data.Num.Bitwise +import Mathlib.Data.Opposite +import Mathlib.Data.Option.Basic +import Mathlib.Data.Option.Defs +import Mathlib.Data.Option.NAry +import Mathlib.Data.PEquiv +import Mathlib.Data.PFun +import Mathlib.Data.PFunctor.Multivariate.Basic +import Mathlib.Data.PFunctor.Univariate.Basic +import Mathlib.Data.PFunctor.Univariate.M +import Mathlib.Data.PNat.Basic +import Mathlib.Data.PNat.Defs +import Mathlib.Data.PNat.Factors +import Mathlib.Data.PNat.Find +import Mathlib.Data.PNat.Interval +import Mathlib.Data.PNat.Prime +import Mathlib.Data.PNat.Xgcd +import Mathlib.Data.PSigma.Order +import Mathlib.Data.Part +import Mathlib.Data.Pi.Algebra +import Mathlib.Data.Pi.Interval +import Mathlib.Data.Pi.Lex +import Mathlib.Data.Prod.Basic +import Mathlib.Data.Prod.Lex +import Mathlib.Data.Prod.PProd +import Mathlib.Data.Prod.TProd +import Mathlib.Data.Quot +import Mathlib.Data.Rat.Basic +import Mathlib.Data.Rat.BigOperators +import Mathlib.Data.Rat.Cast +import Mathlib.Data.Rat.Defs +import Mathlib.Data.Rat.Denumerable +import Mathlib.Data.Rat.Encodable +import Mathlib.Data.Rat.Floor +import Mathlib.Data.Rat.Init +import Mathlib.Data.Rat.Lemmas +import Mathlib.Data.Rat.Order +import Mathlib.Data.Rat.Sqrt +import Mathlib.Data.Real.Basic +import Mathlib.Data.Real.CauSeq +import Mathlib.Data.Real.CauSeqCompletion +import Mathlib.Data.Real.Pointwise +import Mathlib.Data.Real.Sign +import Mathlib.Data.Rel +import Mathlib.Data.Semiquot +import Mathlib.Data.Seq.Computation +import Mathlib.Data.Set.Accumulate +import Mathlib.Data.Set.Basic +import Mathlib.Data.Set.BoolIndicator +import Mathlib.Data.Set.Constructions +import Mathlib.Data.Set.Countable +import Mathlib.Data.Set.Enumerate +import Mathlib.Data.Set.Equitable +import Mathlib.Data.Set.Finite +import Mathlib.Data.Set.Function +import Mathlib.Data.Set.Functor +import Mathlib.Data.Set.Image +import Mathlib.Data.Set.Intervals.Basic +import Mathlib.Data.Set.Intervals.Disjoint +import Mathlib.Data.Set.Intervals.Group +import Mathlib.Data.Set.Intervals.Infinite +import Mathlib.Data.Set.Intervals.Instances +import Mathlib.Data.Set.Intervals.IsoIoo +import Mathlib.Data.Set.Intervals.Monoid +import Mathlib.Data.Set.Intervals.Monotone +import Mathlib.Data.Set.Intervals.OrdConnected +import Mathlib.Data.Set.Intervals.OrdConnectedComponent +import Mathlib.Data.Set.Intervals.OrderIso +import Mathlib.Data.Set.Intervals.Pi +import Mathlib.Data.Set.Intervals.ProjIcc +import Mathlib.Data.Set.Intervals.SurjOn +import Mathlib.Data.Set.Intervals.UnorderedInterval +import Mathlib.Data.Set.Intervals.WithBotTop +import Mathlib.Data.Set.Lattice +import Mathlib.Data.Set.MulAntidiagonal +import Mathlib.Data.Set.NAry +import Mathlib.Data.Set.Opposite +import Mathlib.Data.Set.Pairwise +import Mathlib.Data.Set.Pointwise.Basic +import Mathlib.Data.Set.Pointwise.BigOperators +import Mathlib.Data.Set.Pointwise.Finite +import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Data.Set.Pointwise.Iterate +import Mathlib.Data.Set.Pointwise.ListOfFn +import Mathlib.Data.Set.Pointwise.SMul +import Mathlib.Data.Set.Pointwise.Support +import Mathlib.Data.Set.Prod +import Mathlib.Data.Set.Semiring +import Mathlib.Data.Set.Sigma +import Mathlib.Data.Set.UnionLift +import Mathlib.Data.SetLike.Basic +import Mathlib.Data.SetLike.Fintype +import Mathlib.Data.Setoid.Basic +import Mathlib.Data.Setoid.Partition +import Mathlib.Data.Sigma.Basic +import Mathlib.Data.Sigma.Interval +import Mathlib.Data.Sigma.Lex +import Mathlib.Data.Sigma.Order +import Mathlib.Data.Sign +import Mathlib.Data.Stream.Defs +import Mathlib.Data.Stream.Init +import Mathlib.Data.String.Defs +import Mathlib.Data.String.Lemmas +import Mathlib.Data.Subtype +import Mathlib.Data.Sum.Basic +import Mathlib.Data.Sum.Interval +import Mathlib.Data.Sum.Order +import Mathlib.Data.Sym.Basic +import Mathlib.Data.Sym.Sym2 +import Mathlib.Data.TwoPointing +import Mathlib.Data.TypeVec +import Mathlib.Data.TypeVec.Attr +import Mathlib.Data.UInt +import Mathlib.Data.ULift +import Mathlib.Data.UnionFind +import Mathlib.Data.Vector +import Mathlib.Data.Vector.Basic +import Mathlib.Data.Vector.Mem +import Mathlib.Data.Vector.Zip +import Mathlib.Data.W.Basic +import Mathlib.Data.W.Constructions +import Mathlib.Data.ZMod.Defs +import Mathlib.Deprecated.Group +import Mathlib.Deprecated.Ring +import Mathlib.Deprecated.Subgroup +import Mathlib.Deprecated.Submonoid +import Mathlib.Deprecated.Subring +import Mathlib.Dynamics.FixedPoints.Basic +import Mathlib.Dynamics.FixedPoints.Topology +import Mathlib.Dynamics.Minimal +import Mathlib.Dynamics.PeriodicPts +import Mathlib.GroupTheory.Abelianization +import Mathlib.GroupTheory.Archimedean +import Mathlib.GroupTheory.Commensurable +import Mathlib.GroupTheory.Commutator +import Mathlib.GroupTheory.CommutingProbability +import Mathlib.GroupTheory.Congruence +import Mathlib.GroupTheory.Coset +import Mathlib.GroupTheory.Divisible +import Mathlib.GroupTheory.DoubleCoset +import Mathlib.GroupTheory.EckmannHilton +import Mathlib.GroupTheory.Finiteness +import Mathlib.GroupTheory.FreeGroup +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.GroupAction.BigOperators +import Mathlib.GroupTheory.GroupAction.ConjAct +import Mathlib.GroupTheory.GroupAction.Defs +import Mathlib.GroupTheory.GroupAction.Embedding +import Mathlib.GroupTheory.GroupAction.FixingSubgroup +import Mathlib.GroupTheory.GroupAction.Group +import Mathlib.GroupTheory.GroupAction.Opposite +import Mathlib.GroupTheory.GroupAction.Option +import Mathlib.GroupTheory.GroupAction.Pi +import Mathlib.GroupTheory.GroupAction.Prod +import Mathlib.GroupTheory.GroupAction.Quotient +import Mathlib.GroupTheory.GroupAction.Sigma +import Mathlib.GroupTheory.GroupAction.SubMulAction +import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise +import Mathlib.GroupTheory.GroupAction.Sum +import Mathlib.GroupTheory.GroupAction.Support +import Mathlib.GroupTheory.GroupAction.Units +import Mathlib.GroupTheory.Index +import Mathlib.GroupTheory.IsFreeGroup +import Mathlib.GroupTheory.MonoidLocalization +import Mathlib.GroupTheory.Perm.Basic +import Mathlib.GroupTheory.Perm.List +import Mathlib.GroupTheory.Perm.Subgroup +import Mathlib.GroupTheory.Perm.Support +import Mathlib.GroupTheory.Perm.ViaEmbedding +import Mathlib.GroupTheory.PresentedGroup +import Mathlib.GroupTheory.QuotientGroup +import Mathlib.GroupTheory.SemidirectProduct +import Mathlib.GroupTheory.Subgroup.Actions +import Mathlib.GroupTheory.Subgroup.Basic +import Mathlib.GroupTheory.Subgroup.Finite +import Mathlib.GroupTheory.Subgroup.MulOpposite +import Mathlib.GroupTheory.Subgroup.Pointwise +import Mathlib.GroupTheory.Subgroup.Saturated +import Mathlib.GroupTheory.Subgroup.Simple +import Mathlib.GroupTheory.Subgroup.Zpowers +import Mathlib.GroupTheory.Submonoid.Basic +import Mathlib.GroupTheory.Submonoid.Center +import Mathlib.GroupTheory.Submonoid.Centralizer +import Mathlib.GroupTheory.Submonoid.Inverses +import Mathlib.GroupTheory.Submonoid.Membership +import Mathlib.GroupTheory.Submonoid.Operations +import Mathlib.GroupTheory.Submonoid.Pointwise +import Mathlib.GroupTheory.Subsemigroup.Basic +import Mathlib.GroupTheory.Subsemigroup.Center +import Mathlib.GroupTheory.Subsemigroup.Centralizer +import Mathlib.GroupTheory.Subsemigroup.Membership +import Mathlib.GroupTheory.Subsemigroup.Operations +import Mathlib.Init.Algebra.Classes +import Mathlib.Init.Algebra.Functions +import Mathlib.Init.Algebra.Order +import Mathlib.Init.Align +import Mathlib.Init.CcLemmas +import Mathlib.Init.Classes.Order +import Mathlib.Init.Classical +import Mathlib.Init.Control.Combinators +import Mathlib.Init.Core +import Mathlib.Init.Data.Bool.Basic +import Mathlib.Init.Data.Bool.Lemmas +import Mathlib.Init.Data.Fin.Basic +import Mathlib.Init.Data.Int.Basic +import Mathlib.Init.Data.Int.Bitwise +import Mathlib.Init.Data.Int.DivMod +import Mathlib.Init.Data.Int.Lemmas +import Mathlib.Init.Data.Int.Order +import Mathlib.Init.Data.List.Basic +import Mathlib.Init.Data.List.Instances +import Mathlib.Init.Data.List.Lemmas +import Mathlib.Init.Data.Nat.Basic +import Mathlib.Init.Data.Nat.Bitwise +import Mathlib.Init.Data.Nat.Div +import Mathlib.Init.Data.Nat.GCD +import Mathlib.Init.Data.Nat.Lemmas +import Mathlib.Init.Data.Nat.Notation +import Mathlib.Init.Data.Option.Basic +import Mathlib.Init.Data.Option.Init.Lemmas +import Mathlib.Init.Data.Option.Lemmas +import Mathlib.Init.Data.Ordering.Basic +import Mathlib.Init.Data.Prod +import Mathlib.Init.Data.Quot +import Mathlib.Init.Data.Rat.Basic +import Mathlib.Init.Data.Sigma.Basic +import Mathlib.Init.Data.Subtype.Basic +import Mathlib.Init.Function +import Mathlib.Init.Logic +import Mathlib.Init.Meta.WellFoundedTactics +import Mathlib.Init.Propext +import Mathlib.Init.Quot +import Mathlib.Init.Set +import Mathlib.Init.ZeroOne +import Mathlib.Lean.EnvExtension +import Mathlib.Lean.Exception +import Mathlib.Lean.Expr +import Mathlib.Lean.Expr.Basic +import Mathlib.Lean.Expr.ReplaceRec +import Mathlib.Lean.Expr.Traverse +import Mathlib.Lean.LocalContext +import Mathlib.Lean.Message +import Mathlib.Lean.Meta +import Mathlib.Lean.Meta.Simp +import Mathlib.LinearAlgebra.AffineSpace.Basic +import Mathlib.LinearAlgebra.Basic +import Mathlib.LinearAlgebra.GeneralLinearGroup +import Mathlib.LinearAlgebra.Pi +import Mathlib.LinearAlgebra.Quotient +import Mathlib.LinearAlgebra.Span +import Mathlib.Logic.Basic +import Mathlib.Logic.Denumerable +import Mathlib.Logic.Embedding.Basic +import Mathlib.Logic.Embedding.Set +import Mathlib.Logic.Encodable.Basic +import Mathlib.Logic.Encodable.Lattice +import Mathlib.Logic.Equiv.Basic +import Mathlib.Logic.Equiv.Defs +import Mathlib.Logic.Equiv.Embedding +import Mathlib.Logic.Equiv.Fin +import Mathlib.Logic.Equiv.List +import Mathlib.Logic.Equiv.LocalEquiv +import Mathlib.Logic.Equiv.MfldSimpsAttr +import Mathlib.Logic.Equiv.Nat +import Mathlib.Logic.Equiv.Option +import Mathlib.Logic.Equiv.Set +import Mathlib.Logic.Function.Basic +import Mathlib.Logic.Function.Conjugate +import Mathlib.Logic.Function.Iterate +import Mathlib.Logic.IsEmpty +import Mathlib.Logic.Lemmas +import Mathlib.Logic.Nonempty +import Mathlib.Logic.Nontrivial +import Mathlib.Logic.Pairwise +import Mathlib.Logic.Relation +import Mathlib.Logic.Relator +import Mathlib.Logic.Small.Basic +import Mathlib.Logic.Small.List +import Mathlib.Logic.Unique +import Mathlib.Mathport.Attributes +import Mathlib.Mathport.Notation +import Mathlib.Mathport.Rename +import Mathlib.Mathport.Syntax +import Mathlib.MeasureTheory.MeasurableSpace +import Mathlib.MeasureTheory.MeasurableSpaceDef +import Mathlib.MeasureTheory.PiSystem +import Mathlib.NumberTheory.ADEInequality +import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue +import Mathlib.NumberTheory.Divisors +import Mathlib.NumberTheory.FrobeniusNumber +import Mathlib.NumberTheory.Primorial +import Mathlib.Order.Antichain +import Mathlib.Order.Antisymmetrization +import Mathlib.Order.Atoms +import Mathlib.Order.Atoms.Finite +import Mathlib.Order.Basic +import Mathlib.Order.BooleanAlgebra +import Mathlib.Order.Bounded +import Mathlib.Order.BoundedOrder +import Mathlib.Order.Bounds.Basic +import Mathlib.Order.Bounds.OrderIso +import Mathlib.Order.Chain +import Mathlib.Order.Circular +import Mathlib.Order.Closure +import Mathlib.Order.CompactlyGenerated +import Mathlib.Order.Compare +import Mathlib.Order.CompleteBooleanAlgebra +import Mathlib.Order.CompleteLattice +import Mathlib.Order.CompleteLatticeIntervals +import Mathlib.Order.Concept +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Finset +import Mathlib.Order.ConditionallyCompleteLattice.Group +import Mathlib.Order.Copy +import Mathlib.Order.CountableDenseLinearOrder +import Mathlib.Order.Cover +import Mathlib.Order.Directed +import Mathlib.Order.Disjoint +import Mathlib.Order.Disjointed +import Mathlib.Order.Extension.Linear +import Mathlib.Order.Extension.Well +import Mathlib.Order.Filter.Archimedean +import Mathlib.Order.Filter.AtTopBot +import Mathlib.Order.Filter.Bases +import Mathlib.Order.Filter.Basic +import Mathlib.Order.Filter.Cofinite +import Mathlib.Order.Filter.CountableInter +import Mathlib.Order.Filter.Curry +import Mathlib.Order.Filter.Extr +import Mathlib.Order.Filter.Germ +import Mathlib.Order.Filter.IndicatorFunction +import Mathlib.Order.Filter.Interval +import Mathlib.Order.Filter.Lift +import Mathlib.Order.Filter.ModEq +import Mathlib.Order.Filter.NAry +import Mathlib.Order.Filter.Partial +import Mathlib.Order.Filter.Pi +import Mathlib.Order.Filter.Pointwise +import Mathlib.Order.Filter.Prod +import Mathlib.Order.Filter.SmallSets +import Mathlib.Order.Filter.Ultrafilter +import Mathlib.Order.FixedPoints +import Mathlib.Order.GaloisConnection +import Mathlib.Order.GameAdd +import Mathlib.Order.Grade +import Mathlib.Order.Heyting.Basic +import Mathlib.Order.Heyting.Boundary +import Mathlib.Order.Heyting.Hom +import Mathlib.Order.Heyting.Regular +import Mathlib.Order.Hom.Basic +import Mathlib.Order.Hom.Bounded +import Mathlib.Order.Hom.CompleteLattice +import Mathlib.Order.Hom.Lattice +import Mathlib.Order.Hom.Order +import Mathlib.Order.Hom.Set +import Mathlib.Order.Ideal +import Mathlib.Order.InitialSeg +import Mathlib.Order.Iterate +import Mathlib.Order.Lattice +import Mathlib.Order.LatticeIntervals +import Mathlib.Order.LiminfLimsup +import Mathlib.Order.LocallyFinite +import Mathlib.Order.Max +import Mathlib.Order.MinMax +import Mathlib.Order.Minimal +import Mathlib.Order.ModularLattice +import Mathlib.Order.Monotone.Basic +import Mathlib.Order.Monotone.Extension +import Mathlib.Order.Monotone.Monovary +import Mathlib.Order.Monotone.Odd +import Mathlib.Order.Monotone.Union +import Mathlib.Order.OmegaCompletePartialOrder +import Mathlib.Order.OrdContinuous +import Mathlib.Order.OrderIsoNat +import Mathlib.Order.PFilter +import Mathlib.Order.PartialSups +import Mathlib.Order.Partition.Equipartition +import Mathlib.Order.Partition.Finpartition +import Mathlib.Order.PrimeIdeal +import Mathlib.Order.PropInstances +import Mathlib.Order.RelClasses +import Mathlib.Order.RelIso.Basic +import Mathlib.Order.RelIso.Group +import Mathlib.Order.RelIso.Set +import Mathlib.Order.SemiconjSup +import Mathlib.Order.SuccPred.Basic +import Mathlib.Order.SuccPred.IntervalSucc +import Mathlib.Order.SuccPred.Limit +import Mathlib.Order.SuccPred.LinearLocallyFinite +import Mathlib.Order.SuccPred.Relation +import Mathlib.Order.SupIndep +import Mathlib.Order.SymmDiff +import Mathlib.Order.Synonym +import Mathlib.Order.UpperLower.Basic +import Mathlib.Order.UpperLower.Hom +import Mathlib.Order.WellFounded +import Mathlib.Order.WellFoundedSet +import Mathlib.Order.WithBot +import Mathlib.Order.Zorn +import Mathlib.Order.ZornAtoms +import Mathlib.RingTheory.Congruence +import Mathlib.RingTheory.Coprime.Basic +import Mathlib.RingTheory.Coprime.Lemmas +import Mathlib.RingTheory.Fintype +import Mathlib.RingTheory.NonZeroDivisors +import Mathlib.RingTheory.OreLocalization.Basic +import Mathlib.RingTheory.OreLocalization.OreSet +import Mathlib.RingTheory.Prime +import Mathlib.RingTheory.RingInvo +import Mathlib.RingTheory.Subring.Basic +import Mathlib.RingTheory.Subsemiring.Basic +import Mathlib.RingTheory.Subsemiring.Pointwise +import Mathlib.SetTheory.Cardinal.Basic +import Mathlib.SetTheory.Cardinal.Finite +import Mathlib.SetTheory.Cardinal.SchroederBernstein +import Mathlib.SetTheory.Lists +import Mathlib.SetTheory.Ordinal.Arithmetic +import Mathlib.SetTheory.Ordinal.Basic +import Mathlib.SetTheory.Ordinal.NaturalOps +import Mathlib.SetTheory.Ordinal.Topology +import Mathlib.Tactic.Abel +import Mathlib.Tactic.Alias +import Mathlib.Tactic.ApplyFun +import Mathlib.Tactic.ApplyWith +import Mathlib.Tactic.Basic +import Mathlib.Tactic.ByContra +import Mathlib.Tactic.Cache +import Mathlib.Tactic.Cases +import Mathlib.Tactic.CasesM +import Mathlib.Tactic.Choose +import Mathlib.Tactic.Classical +import Mathlib.Tactic.Clear! +import Mathlib.Tactic.ClearExcept +import Mathlib.Tactic.Clear_ +import Mathlib.Tactic.Coe +import Mathlib.Tactic.Constructor +import Mathlib.Tactic.Continuity +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Conv +import Mathlib.Tactic.Convert +import Mathlib.Tactic.Core +import Mathlib.Tactic.Existsi +import Mathlib.Tactic.Expect +import Mathlib.Tactic.FailIfNoProgress +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Find +import Mathlib.Tactic.GeneralizeProofs +import Mathlib.Tactic.Group +import Mathlib.Tactic.GuardGoalNums +import Mathlib.Tactic.GuardHypNums +import Mathlib.Tactic.Have +import Mathlib.Tactic.HelpCmd +import Mathlib.Tactic.InferParam +import Mathlib.Tactic.Inhabit +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.IrreducibleDef +import Mathlib.Tactic.LabelAttr +import Mathlib.Tactic.LeftRight +import Mathlib.Tactic.LibrarySearch +import Mathlib.Tactic.Lift +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Linarith.Datatypes +import Mathlib.Tactic.Linarith.Elimination +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.Linarith.Lemmas +import Mathlib.Tactic.Linarith.Parsing +import Mathlib.Tactic.Linarith.Preprocessing +import Mathlib.Tactic.Linarith.Verification +import Mathlib.Tactic.LinearCombination +import Mathlib.Tactic.MkIffOfInductiveProp +import Mathlib.Tactic.ModCases +import Mathlib.Tactic.Monotonicity +import Mathlib.Tactic.Monotonicity.Attr +import Mathlib.Tactic.Monotonicity.Basic +import Mathlib.Tactic.Monotonicity.Lemmas +import Mathlib.Tactic.Nontriviality +import Mathlib.Tactic.Nontriviality.Core +import Mathlib.Tactic.NormCast +import Mathlib.Tactic.NormCast.Tactic +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.NormNum.Basic +import Mathlib.Tactic.NormNum.Core +import Mathlib.Tactic.NthRewrite +import Mathlib.Tactic.PermuteGoals +import Mathlib.Tactic.Polyrith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Positivity.Basic +import Mathlib.Tactic.Positivity.Core +import Mathlib.Tactic.PrintPrefix +import Mathlib.Tactic.PushNeg +import Mathlib.Tactic.Qify +import Mathlib.Tactic.Qify.Attr +import Mathlib.Tactic.RSuffices +import Mathlib.Tactic.Reassoc +import Mathlib.Tactic.Recover +import Mathlib.Tactic.Relation.Rfl +import Mathlib.Tactic.Relation.Symm +import Mathlib.Tactic.Relation.Trans +import Mathlib.Tactic.Rename +import Mathlib.Tactic.RenameBVar +import Mathlib.Tactic.Replace +import Mathlib.Tactic.RestateAxiom +import Mathlib.Tactic.Ring +import Mathlib.Tactic.Ring.Basic +import Mathlib.Tactic.Ring.RingNF +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Sat.FromLRAT +import Mathlib.Tactic.ScopedNS +import Mathlib.Tactic.Set +import Mathlib.Tactic.SimpIntro +import Mathlib.Tactic.SimpRw +import Mathlib.Tactic.Simps.Basic +import Mathlib.Tactic.Simps.NotationClass +import Mathlib.Tactic.Slice +import Mathlib.Tactic.SolveByElim +import Mathlib.Tactic.SplitIfs +import Mathlib.Tactic.Spread +import Mathlib.Tactic.Substs +import Mathlib.Tactic.SudoSetOption +import Mathlib.Tactic.SwapVar +import Mathlib.Tactic.Tauto +import Mathlib.Tactic.ToAdditive +import Mathlib.Tactic.Trace +import Mathlib.Tactic.TypeCheck +import Mathlib.Tactic.UnsetOption +import Mathlib.Tactic.Use +import Mathlib.Tactic.WLOG +import Mathlib.Tactic.Zify +import Mathlib.Tactic.Zify.Attr +import Mathlib.Testing.SlimCheck.Gen +import Mathlib.Testing.SlimCheck.Sampleable +import Mathlib.Testing.SlimCheck.Testable +import Mathlib.Topology.Alexandroff +import Mathlib.Topology.Algebra.ConstMulAction +import Mathlib.Topology.Algebra.Constructions +import Mathlib.Topology.Algebra.GroupWithZero +import Mathlib.Topology.Algebra.Monoid +import Mathlib.Topology.Algebra.MulAction +import Mathlib.Topology.Algebra.Order.Archimedean +import Mathlib.Topology.Algebra.Order.Compact +import Mathlib.Topology.Algebra.Order.ExtendFrom +import Mathlib.Topology.Algebra.Order.ExtrClosure +import Mathlib.Topology.Algebra.Order.Filter +import Mathlib.Topology.Algebra.Order.IntermediateValue +import Mathlib.Topology.Algebra.Order.LeftRight +import Mathlib.Topology.Algebra.Order.LeftRightLim +import Mathlib.Topology.Algebra.Order.LiminfLimsup +import Mathlib.Topology.Algebra.Order.MonotoneContinuity +import Mathlib.Topology.Algebra.Order.MonotoneConvergence +import Mathlib.Topology.Algebra.Order.ProjIcc +import Mathlib.Topology.Algebra.Order.T5 +import Mathlib.Topology.Algebra.Semigroup +import Mathlib.Topology.Algebra.Star +import Mathlib.Topology.Bases +import Mathlib.Topology.Basic +import Mathlib.Topology.Bornology.Basic +import Mathlib.Topology.Bornology.Constructions +import Mathlib.Topology.Bornology.Hom +import Mathlib.Topology.CompactOpen +import Mathlib.Topology.Connected +import Mathlib.Topology.Constructions +import Mathlib.Topology.ContinuousFunction.Basic +import Mathlib.Topology.ContinuousFunction.CocompactMap +import Mathlib.Topology.ContinuousFunction.T0Sierpinski +import Mathlib.Topology.ContinuousOn +import Mathlib.Topology.DenseEmbedding +import Mathlib.Topology.DiscreteQuotient +import Mathlib.Topology.ExtendFrom +import Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle +import Mathlib.Topology.Filter +import Mathlib.Topology.GDelta +import Mathlib.Topology.Hom.Open +import Mathlib.Topology.Homeomorph +import Mathlib.Topology.Inseparable +import Mathlib.Topology.Instances.Sign +import Mathlib.Topology.List +import Mathlib.Topology.LocalExtr +import Mathlib.Topology.LocalHomeomorph +import Mathlib.Topology.LocallyConstant.Basic +import Mathlib.Topology.LocallyFinite +import Mathlib.Topology.Maps +import Mathlib.Topology.NhdsSet +import Mathlib.Topology.NoetherianSpace +import Mathlib.Topology.OmegaCompletePartialOrder +import Mathlib.Topology.Order +import Mathlib.Topology.Order.Basic +import Mathlib.Topology.Order.Hom.Basic +import Mathlib.Topology.Order.Lattice +import Mathlib.Topology.Order.LowerTopology +import Mathlib.Topology.Order.Priestley +import Mathlib.Topology.Paracompact +import Mathlib.Topology.Partial +import Mathlib.Topology.Perfect +import Mathlib.Topology.QuasiSeparated +import Mathlib.Topology.Separation +import Mathlib.Topology.Sets.Closeds +import Mathlib.Topology.Sets.Compacts +import Mathlib.Topology.Sets.Opens +import Mathlib.Topology.Sets.Order +import Mathlib.Topology.ShrinkingLemma +import Mathlib.Topology.Sober +import Mathlib.Topology.Spectral.Hom +import Mathlib.Topology.StoneCech +import Mathlib.Topology.SubsetProperties +import Mathlib.Topology.Support +import Mathlib.Topology.UniformSpace.AbsoluteValue +import Mathlib.Topology.UniformSpace.AbstractCompletion +import Mathlib.Topology.UniformSpace.Basic +import Mathlib.Topology.UniformSpace.Cauchy +import Mathlib.Topology.UniformSpace.CompactConvergence +import Mathlib.Topology.UniformSpace.CompleteSeparated +import Mathlib.Topology.UniformSpace.Completion +import Mathlib.Topology.UniformSpace.Equiv +import Mathlib.Topology.UniformSpace.Pi +import Mathlib.Topology.UniformSpace.Separation +import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib.Topology.UniformSpace.UniformEmbedding +import Mathlib.Util.AssertNoSorry +import Mathlib.Util.AtomM +import Mathlib.Util.Export +import Mathlib.Util.IncludeStr +import Mathlib.Util.MemoFix +import Mathlib.Util.Simp +import Mathlib.Util.Syntax +import Mathlib.Util.SynthesizeUsing +import Mathlib.Util.Tactic +import Mathlib.Util.Time +import Mathlib.Util.WhatsNew +import Mathlib.Util.WithWeakNamespace diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean new file mode 100644 index 0000000000000..1c69827598c46 --- /dev/null +++ b/Mathlib/CategoryTheory/Category/Cat.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2019 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov + +! This file was ported from Lean 3 source module category_theory.category.Cat +! leanprover-community/mathlib commit e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.ConcreteCategory.Bundled +import Mathlib.CategoryTheory.DiscreteCategory +import Mathlib.CategoryTheory.Types +import Mathlib.CategoryTheory.Bicategory.Strict + +/-! +# Category of categories + +This file contains the definition of the category `Cat` of all categories. +In this category objects are categories and +morphisms are functors between these categories. + +## Implementation notes + +Though `Cat` is not a concrete category, we use `bundled` to define +its carrier type. +-/ + + +universe v u + +namespace CategoryTheory + +-- intended to be used with explicit universe parameters +/-- Category of categories. -/ +@[nolint checkUnivs] +def Cat := + Bundled Category.{v, u} +set_option linter.uppercaseLean3 false in +#align category_theory.Cat CategoryTheory.Cat + +namespace Cat + +instance : Inhabited Cat := + ⟨⟨Type u, CategoryTheory.types⟩⟩ + +instance : CoeSort Cat (Type u) := + ⟨Bundled.α⟩ + +instance str (C : Cat.{v, u}) : Category.{v, u} C := + Bundled.str C +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.str CategoryTheory.Cat.str + +/-- Construct a bundled `Cat` from the underlying type and the typeclass. -/ +def of (C : Type u) [Category.{v} C] : Cat.{v, u} := + Bundled.of C +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.of CategoryTheory.Cat.of + +/-- Bicategory structure on `Cat` -/ +instance bicategory : Bicategory.{max v u, max v u} Cat.{v, u} + where + Hom C D := C ⥤ D + id C := 𝟭 C + comp F G := F ⋙ G + homCategory := fun _ _ => Functor.category + whiskerLeft {C} {D} {E} F G H η := whiskerLeft F η + whiskerRight {C} {D} {E} F G η H := whiskerRight η H + associator {A} {B} {C} D := Functor.associator + leftUnitor {A} B := Functor.leftUnitor + rightUnitor {A} B := Functor.rightUnitor + pentagon := fun {A} {B} {C} {D} {E}=> Functor.pentagon + triangle {A} {B} {C} := Functor.triangle +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.bicategory CategoryTheory.Cat.bicategory + +/-- `Cat` is a strict bicategory. -/ +instance bicategory.strict : Bicategory.Strict Cat.{v, u} where + id_comp {C} {D} F := by cases F; rfl + comp_id {C} {D} F := by cases F; rfl + assoc := by intros; rfl +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.bicategory.strict CategoryTheory.Cat.bicategory.strict + +/-- Category structure on `Cat` -/ +instance category : LargeCategory.{max v u} Cat.{v, u} := + StrictBicategory.category Cat.{v, u} +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.category CategoryTheory.Cat.category + +@[simp] +theorem id_map {C : Cat} {X Y : C} (f : X ⟶ Y) : (𝟙 C : C ⥤ C).map f = f := + Functor.id_map f +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.id_map CategoryTheory.Cat.id_map + +@[simp] +theorem comp_obj {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) (X : C) : (F ≫ G).obj X = G.obj (F.obj X) := + Functor.comp_obj F G X +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.comp_obj CategoryTheory.Cat.comp_obj + +@[simp] +theorem comp_map {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : C} (f : X ⟶ Y) : + (F ≫ G).map f = G.map (F.map f) := + Functor.comp_map F G f +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.comp_map CategoryTheory.Cat.comp_map + +/-- Functor that gets the set of objects of a category. It is not +called `forget`, because it is not a faithful functor. -/ +def objects : Cat.{v, u} ⥤ Type u where + obj C := C + map F := F.obj +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.objects CategoryTheory.Cat.objects + +section + +attribute [local simp] eqToHom_map + +/-- Any isomorphism in `Cat` induces an equivalence of the underlying categories. -/ +def equivOfIso {C D : Cat} (γ : C ≅ D) : C ≌ D + where + functor := γ.hom + inverse := γ.inv + unitIso := eqToIso <| Eq.symm γ.hom_inv_id + counitIso := eqToIso γ.inv_hom_id +set_option linter.uppercaseLean3 false in +#align category_theory.Cat.equiv_of_iso CategoryTheory.Cat.equivOfIso + +end + +end Cat + +/-- Embedding `Type` into `Cat` as discrete categories. + +This ought to be modelled as a 2-functor! +-/ +@[simps] +def typeToCat : Type u ⥤ Cat where + obj X := Cat.of (Discrete X) + map := fun {X} {Y} f => by + dsimp + exact Discrete.functor (Discrete.mk ∘ f) + map_id X := by + apply Functor.ext + · intro X Y f + cases f + simp only [id_eq, eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp] + apply ULift.ext + aesop_cat + · aesop_cat + map_comp f g := by apply Functor.ext; aesop_cat +set_option linter.uppercaseLean3 false in +#align category_theory.Type_to_Cat CategoryTheory.typeToCat + +instance : Faithful typeToCat.{u} where + map_injective {_X} {_Y} _f _g h := + funext fun x => congr_arg Discrete.as (Functor.congr_obj h ⟨x⟩) + +instance : Full typeToCat.{u} + where + preimage F := Discrete.as ∘ F.obj ∘ Discrete.mk + witness := by + intro X Y F + apply Functor.ext + · intro x y f + dsimp + apply ULift.ext + aesop_cat + · rintro ⟨x⟩ + apply Discrete.ext + rfl + +end CategoryTheory + diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean new file mode 100644 index 0000000000000..cac60eb13ddee --- /dev/null +++ b/Mathlib/CategoryTheory/DiscreteCategory.lean @@ -0,0 +1,364 @@ +/- +Copyright (c) 2017 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Stephen Morgan, Scott Morrison, Floris van Doorn + +! This file was ported from Lean 3 source module category_theory.discrete_category +! leanprover-community/mathlib commit 369525b73f229ccd76a6ec0e0e0bf2be57599768 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.EqToHom +import Mathlib.Data.ULift +import Mathlib.Tactic.CasesM + +/-! +# Discrete categories + +We define `Discrete α` as a structure containing a term `a : α` for any type `α`, +and use this type alias to provide a `SmallCategory` instance +whose only morphisms are the identities. + +There is an annoying technical difficulty that it has turned out to be inconvenient +to allow categories with morphisms living in `Prop`, +so instead of defining `X ⟶ Y` in `Discrete α` as `X = Y`, +one might define it as `PLift (X = Y)`. +In fact, to allow `Discrete α` to be a `SmallCategory` +(i.e. with morphisms in the same universe as the objects), +we actually define the hom type `X ⟶ Y` as `ULift (PLift (X = Y))`. + +`Discrete.functor` promotes a function `f : I → C` (for any category `C`) to a functor +`Discrete.functor f : Discrete I ⥤ C`. + +Similarly, `Discrete.natTrans` and `Discrete.natIso` promote `I`-indexed families of morphisms, +or `I`-indexed families of isomorphisms to natural transformations or natural isomorphism. + +We show equivalences of types are the same as (categorical) equivalences of the corresponding +discrete categories. +-/ + +namespace CategoryTheory + +-- morphism levels before object levels. See note [CategoryTheory universes]. +universe v₁ v₂ v₃ u₁ u₁' u₂ u₃ + +-- This is intentionally a structure rather than a type synonym +-- to enforce using `DiscreteEquiv` (or `Discrete.mk` and `Discrete.as`) to move between +-- `discrete α` and `α`. Otherwise there is too much API leakage. +/-- A wrapper for promoting any type to a category, +with the only morphisms being equalities. +-/ +@[ext] +structure Discrete (α : Type u₁) where + /-- A wrapper for promoting any type to a category, + with the only morphisms being equalities. + -/ + as : α +#align category_theory.discrete CategoryTheory.Discrete + +@[simp] +theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X := by + ext + rfl +#align category_theory.discrete.mk_as CategoryTheory.Discrete.mk_as + +/-- `Discrete α` is equivalent to the original type `α`.-/ +@[simps] +def discreteEquiv {α : Type u₁} : Discrete α ≃ α + where + toFun := Discrete.as + invFun := Discrete.mk + left_inv := by aesop_cat + right_inv := by aesop_cat +#align category_theory.discrete_equiv CategoryTheory.discreteEquiv + +instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) := + discreteEquiv.decidableEq + +/-- The "Discrete" category on a type, whose morphisms are equalities. + +Because we do not allow morphisms in `Prop` (only in `Type`), +somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`. + +See +-/ +instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) + where + Hom X Y := ULift (PLift (X.as = Y.as)) + id X := ULift.up (PLift.up rfl) + comp {X Y Z} g f := by + cases X + cases Y + cases Z + rcases f with ⟨⟨⟨⟩⟩⟩ + exact g +#align category_theory.discrete_category CategoryTheory.discreteCategory + +namespace Discrete + +variable {α : Type u₁} + +instance [Inhabited α] : Inhabited (Discrete α) := + ⟨⟨default⟩⟩ + +instance [Subsingleton α] : Subsingleton (Discrete α) := + ⟨by + intros + ext + apply Subsingleton.elim⟩ + +/- ./././Mathport/Syntax/Translate/Expr.lean:334:4: warning: unsupported (TODO): `[tacs] -/ +/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/ +--unsafe def _root_.tactic.discrete_cases : tactic Unit := +-- sorry +--#align tactic.discrete_cases tactic.discrete_cases + + +--run_cmd +-- add_interactive [`` tactic.discrete_cases] + +--attribute [local tidy] tactic.discrete_cases +--`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]] + +--macro (name := discrete_cases) "discrete_cases" : tactic => +-- `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _) +/- Porting note: rewrote `discrete_cases` tactic -/ +macro "discrete_cases": tactic => + `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _) + +instance [Unique α] : Unique (Discrete α) := + Unique.mk' (Discrete α) + +/-- Extract the equation from a morphism in a discrete category. -/ +theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as := + i.down.down +#align category_theory.discrete.eq_of_hom CategoryTheory.Discrete.eq_of_hom + +/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to a morphism `X ⟶ Y` +in the discrete category. -/ +protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y := + eqToHom + (by + ext + exact h) +#align category_theory.discrete.eq_to_hom CategoryTheory.Discrete.eqToHom + +/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to an isomorphism `X ≅ Y` +in the discrete category. -/ +protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y := + eqToIso + (by + ext + exact h) +#align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso + +/-- A variant of `eq_to_hom` that lifts terms to the discrete category. -/ +abbrev eqToHom' {a b : α} (h : a = b) : Discrete.mk a ⟶ Discrete.mk b := + Discrete.eqToHom h +#align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom' + +/-- A variant of `eqToIso` that lifts terms to the discrete category. -/ +abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b := + Discrete.eqToIso h +#align category_theory.discrete.eq_to_iso' CategoryTheory.Discrete.eqToIso' + +@[simp] +theorem id_def (X : Discrete α) : ULift.up (PLift.up (Eq.refl X.as)) = 𝟙 X := + rfl +#align category_theory.discrete.id_def CategoryTheory.Discrete.id_def + +variable {C : Type u₂} [Category.{v₂} C] + +instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f := + ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩ + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- Any function `I → C` gives a functor `Discrete I ⥤ C`. +-/ +def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C + where + obj := F ∘ Discrete.as + map {X Y} f := by + dsimp + rcases f with ⟨⟨h⟩⟩ + exact eqToHom (congrArg _ h) + map_id := by aesop_cat + map_comp := fun {X Y Z} f g => by + discrete_cases + aesop_cat +#align category_theory.discrete.functor CategoryTheory.Discrete.functor + +@[simp] +theorem functor_obj {I : Type u₁} (F : I → C) (i : I) : + (Discrete.functor F).obj (Discrete.mk i) = F i := + rfl +#align category_theory.discrete.functor_obj CategoryTheory.Discrete.functor_obj + +theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) : + (Discrete.functor F).map f = 𝟙 (F i.as) := by aesop_cat +#align category_theory.discrete.functor_map CategoryTheory.Discrete.functor_map + +/-- The discrete functor induced by a composition of maps can be written as a +composition of two discrete functors. +-/ +@[simps!] +def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : + Discrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f := + NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat) +#align category_theory.discrete.functor_comp CategoryTheory.Discrete.functorComp + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- For functors out of a discrete category, +a natural transformation is just a collection of maps, +as the naturality squares are trivial. +-/ +@[simps] +def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G + where + app := f + naturality {X Y} g := by + rcases g with ⟨⟨g⟩⟩ + discrete_cases + rcases g + change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _) + simp +#align category_theory.discrete.nat_trans CategoryTheory.Discrete.natTrans + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- For functors out of a discrete category, +a natural isomorphism is just a collection of isomorphisms, +as the naturality squares are trivial. +-/ +@[simps!] +def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G := + NatIso.ofComponents f fun g => by + rcases g with ⟨⟨g⟩⟩ + discrete_cases + rcases g + change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _) + simp +#align category_theory.discrete.nat_iso CategoryTheory.Discrete.natIso + +@[simp] +theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) + (i : Discrete I) : (Discrete.natIso f).app i = f i := by aesop_cat +#align category_theory.discrete.nat_iso_app CategoryTheory.Discrete.natIso_app + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to + `discrete.functor (F.obj)`. -/ +@[simp] +def natIsoFunctor {I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk) := + natIso fun _ => Iso.refl _ +#align category_theory.discrete.nat_iso_functor CategoryTheory.Discrete.natIsoFunctor + +/-- Composing `discrete.functor F` with another functor `G` amounts to composing `F` with `G.obj` -/ +@[simp] +def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : I → C) (G : C ⥤ D) : + Discrete.functor F ⋙ G ≅ Discrete.functor (G.obj ∘ F) := + natIso fun _ => Iso.refl _ +#align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- We can promote a type-level `equiv` to +an equivalence between the corresponding `discrete` categories. +-/ +@[simps] +def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J + where + functor := Discrete.functor (Discrete.mk ∘ (e : I → J)) + inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I)) + unitIso := + Discrete.natIso fun i => + eqToIso + (by + discrete_cases + simp) + counitIso := + Discrete.natIso fun j => + eqToIso + (by + discrete_cases + simp) +#align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence + +/-- We can convert an equivalence of `discrete` categories to a type-level `equiv`. -/ +@[simps] +def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β + where + toFun := Discrete.as ∘ h.functor.obj ∘ Discrete.mk + invFun := Discrete.as ∘ h.inverse.obj ∘ Discrete.mk + left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2 + right_inv a := by simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1 +#align category_theory.discrete.equiv_of_equivalence CategoryTheory.Discrete.equivOfEquivalence + +end Discrete + +namespace Discrete + +variable {J : Type v₁} + +open Opposite + +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported +\ non-interactive tactic tactic.op_induction' -/ +/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported +\ tactic `discrete_cases #[] -/ +/-- A discrete category is equivalent to its opposite category. -/ +@[simps! functor_obj_as inverse_obj] +protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α := + let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x) + Equivalence.mk F.leftOp F + (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _) + <| fun {X Y} f => by + induction X using Opposite.rec + induction Y using Opposite.rec + rcases f with ⟨⟨f⟩⟩ + discrete_cases + rcases f + aesop_cat) + (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _) +/- + refine' + Equivalence.mk (F.leftOp) F _ + (Discrete.natIso fun X => + by + discrete_cases + rfl) + refine' + NatIso.ofComponents + (fun X => + by + discrete_cases + induction X using Opposite.rec + discrete_cases + exact Iso.refl _) +-/ + +#align category_theory.discrete.opposite CategoryTheory.Discrete.opposite + +variable {C : Type u₂} [Category.{v₂} C] + +@[simp] +theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) := + by + have h : f = 𝟙 j := by + rcases f with ⟨⟨f⟩⟩ + rfl + rw [h] + simp +#align category_theory.discrete.functor_map_id CategoryTheory.Discrete.functor_map_id + +end Discrete + +end CategoryTheory + From acc53943eedb6feb4a13c3055f101ca663d94a54 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 09:41:55 -0500 Subject: [PATCH 5/9] fix weird merge --- Mathlib.lean | 11 - Mathlib.lean.orig | 1197 --------------------------------------------- 2 files changed, 1208 deletions(-) delete mode 100644 Mathlib.lean.orig diff --git a/Mathlib.lean b/Mathlib.lean index 70c113f8041e1..358c67d94da41 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -97,7 +97,6 @@ import Mathlib.Algebra.Homology.ComplexShape import Mathlib.Algebra.IndicatorFunction import Mathlib.Algebra.Invertible import Mathlib.Algebra.IsPrimePow -import Mathlib.Algebra.Module.Algebra import Mathlib.Algebra.Module.Basic import Mathlib.Algebra.Module.BigOperators import Mathlib.Algebra.Module.Equiv @@ -265,7 +264,6 @@ import Mathlib.CategoryTheory.Sigma.Basic import Mathlib.CategoryTheory.Thin import Mathlib.CategoryTheory.Types import Mathlib.CategoryTheory.Whiskering -import Mathlib.CategoryTheory.Yoneda import Mathlib.Combinatorics.Additive.Energy import Mathlib.Combinatorics.Additive.RuzsaCovering import Mathlib.Combinatorics.Colex @@ -509,7 +507,6 @@ import Mathlib.Data.Multiset.FinsetOps import Mathlib.Data.Multiset.Fintype import Mathlib.Data.Multiset.Fold import Mathlib.Data.Multiset.Functor -import Mathlib.Data.Multiset.Interval import Mathlib.Data.Multiset.Lattice import Mathlib.Data.Multiset.LocallyFinite import Mathlib.Data.Multiset.NatAntidiagonal @@ -574,8 +571,6 @@ import Mathlib.Data.Option.NAry import Mathlib.Data.PEquiv import Mathlib.Data.PFun import Mathlib.Data.PFunctor.Multivariate.Basic -import Mathlib.Data.PFunctor.Multivariate.M -import Mathlib.Data.PFunctor.Multivariate.W import Mathlib.Data.PFunctor.Univariate.Basic import Mathlib.Data.PFunctor.Univariate.M import Mathlib.Data.PNat.Basic @@ -594,7 +589,6 @@ import Mathlib.Data.Prod.Basic import Mathlib.Data.Prod.Lex import Mathlib.Data.Prod.PProd import Mathlib.Data.Prod.TProd -import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Data.Quot import Mathlib.Data.Rat.Basic import Mathlib.Data.Rat.BigOperators @@ -610,7 +604,6 @@ import Mathlib.Data.Rat.Sqrt import Mathlib.Data.Real.Basic import Mathlib.Data.Real.CauSeq import Mathlib.Data.Real.CauSeqCompletion -import Mathlib.Data.Real.NNReal import Mathlib.Data.Real.Pointwise import Mathlib.Data.Real.Sign import Mathlib.Data.Rel @@ -857,7 +850,6 @@ import Mathlib.MeasureTheory.MeasurableSpace import Mathlib.MeasureTheory.MeasurableSpaceDef import Mathlib.MeasureTheory.PiSystem import Mathlib.NumberTheory.ADEInequality -import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue import Mathlib.NumberTheory.Divisors import Mathlib.NumberTheory.FrobeniusNumber @@ -900,7 +892,6 @@ import Mathlib.Order.Filter.Cofinite import Mathlib.Order.Filter.CountableInter import Mathlib.Order.Filter.Curry import Mathlib.Order.Filter.Extr -import Mathlib.Order.Filter.FilterProduct import Mathlib.Order.Filter.Germ import Mathlib.Order.Filter.IndicatorFunction import Mathlib.Order.Filter.Interval @@ -990,7 +981,6 @@ import Mathlib.SetTheory.Cardinal.SchroederBernstein import Mathlib.SetTheory.Lists import Mathlib.SetTheory.Ordinal.Arithmetic import Mathlib.SetTheory.Ordinal.Basic -import Mathlib.SetTheory.Ordinal.Exponential import Mathlib.SetTheory.Ordinal.NaturalOps import Mathlib.SetTheory.Ordinal.Topology import Mathlib.Tactic.Abel @@ -1149,7 +1139,6 @@ import Mathlib.Topology.Hom.Open import Mathlib.Topology.Homeomorph import Mathlib.Topology.Inseparable import Mathlib.Topology.Instances.Sign -import Mathlib.Topology.IsLocallyHomeomorph import Mathlib.Topology.List import Mathlib.Topology.LocalExtr import Mathlib.Topology.LocalHomeomorph diff --git a/Mathlib.lean.orig b/Mathlib.lean.orig deleted file mode 100644 index b65b902d4a6d0..0000000000000 --- a/Mathlib.lean.orig +++ /dev/null @@ -1,1197 +0,0 @@ -import Mathlib.Algebra.Abs -import Mathlib.Algebra.AddTorsor -import Mathlib.Algebra.Algebra.Basic -import Mathlib.Algebra.Associated -import Mathlib.Algebra.BigOperators.Associated -import Mathlib.Algebra.BigOperators.Basic -import Mathlib.Algebra.BigOperators.Fin -import Mathlib.Algebra.BigOperators.Finprod -import Mathlib.Algebra.BigOperators.Finsupp -import Mathlib.Algebra.BigOperators.Intervals -import Mathlib.Algebra.BigOperators.Multiset.Basic -import Mathlib.Algebra.BigOperators.Multiset.Lemmas -import Mathlib.Algebra.BigOperators.NatAntidiagonal -import Mathlib.Algebra.BigOperators.Option -import Mathlib.Algebra.BigOperators.Order -import Mathlib.Algebra.BigOperators.Pi -import Mathlib.Algebra.BigOperators.Ring -import Mathlib.Algebra.BigOperators.RingEquiv -import Mathlib.Algebra.Bounds -import Mathlib.Algebra.CharZero.Defs -import Mathlib.Algebra.CharZero.Infinite -import Mathlib.Algebra.CharZero.Lemmas -import Mathlib.Algebra.CharZero.Quotient -import Mathlib.Algebra.CovariantAndContravariant -import Mathlib.Algebra.DirectSum.Basic -import Mathlib.Algebra.Divisibility.Basic -import Mathlib.Algebra.Divisibility.Units -import Mathlib.Algebra.EuclideanDomain.Basic -import Mathlib.Algebra.EuclideanDomain.Defs -import Mathlib.Algebra.EuclideanDomain.Instances -import Mathlib.Algebra.Field.Basic -import Mathlib.Algebra.Field.Defs -import Mathlib.Algebra.Field.Opposite -import Mathlib.Algebra.Field.Power -import Mathlib.Algebra.Free -import Mathlib.Algebra.FreeMonoid.Basic -import Mathlib.Algebra.FreeMonoid.Count -import Mathlib.Algebra.GCDMonoid.Basic -import Mathlib.Algebra.GCDMonoid.Finset -import Mathlib.Algebra.GCDMonoid.Multiset -import Mathlib.Algebra.GeomSum -import Mathlib.Algebra.GradedMonoid -import Mathlib.Algebra.GradedMulAction -import Mathlib.Algebra.Group.Basic -import Mathlib.Algebra.Group.Commutator -import Mathlib.Algebra.Group.Commute -import Mathlib.Algebra.Group.Conj -import Mathlib.Algebra.Group.ConjFinite -import Mathlib.Algebra.Group.Defs -import Mathlib.Algebra.Group.Ext -import Mathlib.Algebra.Group.InjSurj -import Mathlib.Algebra.Group.Opposite -import Mathlib.Algebra.Group.OrderSynonym -import Mathlib.Algebra.Group.Pi -import Mathlib.Algebra.Group.Prod -import Mathlib.Algebra.Group.Semiconj -import Mathlib.Algebra.Group.TypeTags -import Mathlib.Algebra.Group.ULift -import Mathlib.Algebra.Group.UniqueProds -import Mathlib.Algebra.Group.Units -import Mathlib.Algebra.Group.WithOne.Basic -import Mathlib.Algebra.Group.WithOne.Defs -import Mathlib.Algebra.Group.WithOne.Units -import Mathlib.Algebra.GroupPower.Basic -import Mathlib.Algebra.GroupPower.Identities -import Mathlib.Algebra.GroupPower.Lemmas -import Mathlib.Algebra.GroupPower.Order -import Mathlib.Algebra.GroupPower.Ring -import Mathlib.Algebra.GroupRingAction.Basic -import Mathlib.Algebra.GroupRingAction.Subobjects -import Mathlib.Algebra.GroupWithZero.Basic -import Mathlib.Algebra.GroupWithZero.Commute -import Mathlib.Algebra.GroupWithZero.Defs -import Mathlib.Algebra.GroupWithZero.Divisibility -import Mathlib.Algebra.GroupWithZero.InjSurj -import Mathlib.Algebra.GroupWithZero.Power -import Mathlib.Algebra.GroupWithZero.Semiconj -import Mathlib.Algebra.GroupWithZero.Units.Basic -import Mathlib.Algebra.GroupWithZero.Units.Lemmas -import Mathlib.Algebra.HierarchyDesign -import Mathlib.Algebra.Hom.Aut -import Mathlib.Algebra.Hom.Centroid -import Mathlib.Algebra.Hom.Commute -import Mathlib.Algebra.Hom.Embedding -import Mathlib.Algebra.Hom.Equiv.Basic -import Mathlib.Algebra.Hom.Equiv.TypeTags -import Mathlib.Algebra.Hom.Equiv.Units.Basic -import Mathlib.Algebra.Hom.Equiv.Units.GroupWithZero -import Mathlib.Algebra.Hom.Freiman -import Mathlib.Algebra.Hom.Group -import Mathlib.Algebra.Hom.GroupAction -import Mathlib.Algebra.Hom.GroupInstances -import Mathlib.Algebra.Hom.Iterate -import Mathlib.Algebra.Hom.Ring -import Mathlib.Algebra.Hom.Units -import Mathlib.Algebra.Homology.ComplexShape -import Mathlib.Algebra.IndicatorFunction -import Mathlib.Algebra.Invertible -import Mathlib.Algebra.IsPrimePow -import Mathlib.Algebra.Module.Basic -import Mathlib.Algebra.Module.BigOperators -import Mathlib.Algebra.Module.Equiv -import Mathlib.Algebra.Module.Hom -import Mathlib.Algebra.Module.LinearMap -import Mathlib.Algebra.Module.Opposites -import Mathlib.Algebra.Module.Pi -import Mathlib.Algebra.Module.PointwisePi -import Mathlib.Algebra.Module.Prod -import Mathlib.Algebra.Module.Submodule.Basic -import Mathlib.Algebra.Module.Submodule.Lattice -import Mathlib.Algebra.Module.Submodule.Pointwise -import Mathlib.Algebra.Module.ULift -import Mathlib.Algebra.NeZero -import Mathlib.Algebra.Opposites -import Mathlib.Algebra.Order.AbsoluteValue -import Mathlib.Algebra.Order.Archimedean -import Mathlib.Algebra.Order.EuclideanAbsoluteValue -import Mathlib.Algebra.Order.Field.Basic -import Mathlib.Algebra.Order.Field.Canonical.Basic -import Mathlib.Algebra.Order.Field.Canonical.Defs -import Mathlib.Algebra.Order.Field.Defs -import Mathlib.Algebra.Order.Field.InjSurj -import Mathlib.Algebra.Order.Field.Pi -import Mathlib.Algebra.Order.Field.Power -import Mathlib.Algebra.Order.Floor -import Mathlib.Algebra.Order.Group.Abs -import Mathlib.Algebra.Order.Group.Bounds -import Mathlib.Algebra.Order.Group.Defs -import Mathlib.Algebra.Order.Group.DenselyOrdered -import Mathlib.Algebra.Order.Group.InjSurj -import Mathlib.Algebra.Order.Group.Instances -import Mathlib.Algebra.Order.Group.MinMax -import Mathlib.Algebra.Order.Group.OrderIso -import Mathlib.Algebra.Order.Group.Prod -import Mathlib.Algebra.Order.Group.TypeTags -import Mathlib.Algebra.Order.Group.Units -import Mathlib.Algebra.Order.Group.WithTop -import Mathlib.Algebra.Order.Hom.Basic -import Mathlib.Algebra.Order.Hom.Monoid -import Mathlib.Algebra.Order.Invertible -import Mathlib.Algebra.Order.Kleene -import Mathlib.Algebra.Order.LatticeGroup -import Mathlib.Algebra.Order.Module -import Mathlib.Algebra.Order.Monoid.Basic -import Mathlib.Algebra.Order.Monoid.Cancel.Basic -import Mathlib.Algebra.Order.Monoid.Cancel.Defs -import Mathlib.Algebra.Order.Monoid.Canonical.Defs -import Mathlib.Algebra.Order.Monoid.Defs -import Mathlib.Algebra.Order.Monoid.Lemmas -import Mathlib.Algebra.Order.Monoid.MinMax -import Mathlib.Algebra.Order.Monoid.NatCast -import Mathlib.Algebra.Order.Monoid.OrderDual -import Mathlib.Algebra.Order.Monoid.Prod -import Mathlib.Algebra.Order.Monoid.ToMulBot -import Mathlib.Algebra.Order.Monoid.TypeTags -import Mathlib.Algebra.Order.Monoid.Units -import Mathlib.Algebra.Order.Monoid.WithTop -import Mathlib.Algebra.Order.Monoid.WithZero.Basic -import Mathlib.Algebra.Order.Monoid.WithZero.Defs -import Mathlib.Algebra.Order.Nonneg.Field -import Mathlib.Algebra.Order.Nonneg.Ring -import Mathlib.Algebra.Order.Pi -import Mathlib.Algebra.Order.Pointwise -import Mathlib.Algebra.Order.Positive.Field -import Mathlib.Algebra.Order.Positive.Ring -import Mathlib.Algebra.Order.Ring.Abs -import Mathlib.Algebra.Order.Ring.Canonical -import Mathlib.Algebra.Order.Ring.CharZero -import Mathlib.Algebra.Order.Ring.Cone -import Mathlib.Algebra.Order.Ring.Defs -import Mathlib.Algebra.Order.Ring.InjSurj -import Mathlib.Algebra.Order.Ring.Lemmas -import Mathlib.Algebra.Order.Ring.WithTop -import Mathlib.Algebra.Order.SMul -import Mathlib.Algebra.Order.Sub.Basic -import Mathlib.Algebra.Order.Sub.Canonical -import Mathlib.Algebra.Order.Sub.Defs -import Mathlib.Algebra.Order.Sub.WithTop -import Mathlib.Algebra.Order.UpperLower -import Mathlib.Algebra.Order.WithZero -import Mathlib.Algebra.Order.ZeroLEOne -import Mathlib.Algebra.PEmptyInstances -import Mathlib.Algebra.PUnitInstances -import Mathlib.Algebra.Parity -import Mathlib.Algebra.Periodic -import Mathlib.Algebra.Quandle -import Mathlib.Algebra.Quotient -import Mathlib.Algebra.Regular.Basic -import Mathlib.Algebra.Regular.Pow -import Mathlib.Algebra.Regular.SMul -import Mathlib.Algebra.Ring.AddAut -import Mathlib.Algebra.Ring.Aut -import Mathlib.Algebra.Ring.Basic -import Mathlib.Algebra.Ring.Commute -import Mathlib.Algebra.Ring.CompTypeclasses -import Mathlib.Algebra.Ring.Defs -import Mathlib.Algebra.Ring.Divisibility -import Mathlib.Algebra.Ring.Equiv -import Mathlib.Algebra.Ring.Fin -import Mathlib.Algebra.Ring.Idempotents -import Mathlib.Algebra.Ring.InjSurj -import Mathlib.Algebra.Ring.Opposite -import Mathlib.Algebra.Ring.OrderSynonym -import Mathlib.Algebra.Ring.Pi -import Mathlib.Algebra.Ring.Prod -import Mathlib.Algebra.Ring.Regular -import Mathlib.Algebra.Ring.Semiconj -import Mathlib.Algebra.Ring.ULift -import Mathlib.Algebra.Ring.Units -import Mathlib.Algebra.SMulWithZero -import Mathlib.Algebra.Star.Basic -import Mathlib.Algebra.Star.BigOperators -import Mathlib.Algebra.Star.Pi -import Mathlib.Algebra.Star.Pointwise -import Mathlib.Algebra.Star.Prod -import Mathlib.Algebra.Star.SelfAdjoint -import Mathlib.Algebra.Star.Unitary -import Mathlib.Algebra.Support -import Mathlib.Algebra.Tropical.Basic -import Mathlib.Algebra.Tropical.BigOperators -import Mathlib.Algebra.Tropical.Lattice -import Mathlib.CategoryTheory.Arrow -import Mathlib.CategoryTheory.Balanced -import Mathlib.CategoryTheory.Bicategory.Basic -import Mathlib.CategoryTheory.Bicategory.Strict -import Mathlib.CategoryTheory.Category.Basic -import Mathlib.CategoryTheory.Category.Cat -import Mathlib.CategoryTheory.Category.KleisliCat -import Mathlib.CategoryTheory.Category.Preorder -import Mathlib.CategoryTheory.Category.RelCat -import Mathlib.CategoryTheory.Comma -import Mathlib.CategoryTheory.ConcreteCategory.Bundled -<<<<<<< HEAD -import Mathlib.CategoryTheory.Conj -import Mathlib.CategoryTheory.Core -======= -import Mathlib.CategoryTheory.DiscreteCategory ->>>>>>> port/CategoryTheory.DiscreteCategory -import Mathlib.CategoryTheory.Endomorphism -import Mathlib.CategoryTheory.EpiMono -import Mathlib.CategoryTheory.EqToHom -import Mathlib.CategoryTheory.Equivalence -import Mathlib.CategoryTheory.EssentialImage -import Mathlib.CategoryTheory.FullSubcategory -import Mathlib.CategoryTheory.Functor.Basic -import Mathlib.CategoryTheory.Functor.Category -import Mathlib.CategoryTheory.Functor.Const -import Mathlib.CategoryTheory.Functor.Currying -import Mathlib.CategoryTheory.Functor.Default -import Mathlib.CategoryTheory.Functor.FullyFaithful -import Mathlib.CategoryTheory.Functor.Functorial -import Mathlib.CategoryTheory.Functor.Hom -import Mathlib.CategoryTheory.Functor.InvIsos -import Mathlib.CategoryTheory.Groupoid -import Mathlib.CategoryTheory.Groupoid.Basic -import Mathlib.CategoryTheory.Iso -import Mathlib.CategoryTheory.Monoidal.Category -import Mathlib.CategoryTheory.NatIso -import Mathlib.CategoryTheory.NatTrans -import Mathlib.CategoryTheory.Opposites -import Mathlib.CategoryTheory.Pi.Basic -import Mathlib.CategoryTheory.Products.Associator -import Mathlib.CategoryTheory.Products.Basic -import Mathlib.CategoryTheory.Products.Bifunctor -import Mathlib.CategoryTheory.Sigma.Basic -import Mathlib.CategoryTheory.Thin -import Mathlib.CategoryTheory.Types -import Mathlib.CategoryTheory.Whiskering -import Mathlib.Combinatorics.Additive.Energy -import Mathlib.Combinatorics.Additive.RuzsaCovering -import Mathlib.Combinatorics.Colex -import Mathlib.Combinatorics.Composition -import Mathlib.Combinatorics.DoubleCounting -import Mathlib.Combinatorics.Hall.Finite -import Mathlib.Combinatorics.Partition -import Mathlib.Combinatorics.Pigeonhole -import Mathlib.Combinatorics.Quiver.Arborescence -import Mathlib.Combinatorics.Quiver.Basic -import Mathlib.Combinatorics.Quiver.Cast -import Mathlib.Combinatorics.Quiver.ConnectedComponent -import Mathlib.Combinatorics.Quiver.Path -import Mathlib.Combinatorics.Quiver.Push -import Mathlib.Combinatorics.Quiver.SingleObj -import Mathlib.Combinatorics.Quiver.Subquiver -import Mathlib.Combinatorics.Quiver.Symmetric -import Mathlib.Combinatorics.SetFamily.Compression.Down -import Mathlib.Combinatorics.SetFamily.Compression.UV -import Mathlib.Combinatorics.SetFamily.HarrisKleitman -import Mathlib.Combinatorics.SetFamily.Intersecting -import Mathlib.Combinatorics.SetFamily.Kleitman -import Mathlib.Combinatorics.SetFamily.LYM -import Mathlib.Combinatorics.SetFamily.Shadow -import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise -import Mathlib.Combinatorics.Young.SemistandardTableau -import Mathlib.Combinatorics.Young.YoungDiagram -import Mathlib.Computability.DFA -import Mathlib.Computability.Language -import Mathlib.Computability.NFA -import Mathlib.Computability.TuringMachine -import Mathlib.Control.Applicative -import Mathlib.Control.Basic -import Mathlib.Control.EquivFunctor -import Mathlib.Control.EquivFunctor.Instances -import Mathlib.Control.Fix -import Mathlib.Control.Functor -import Mathlib.Control.Functor.Multivariate -import Mathlib.Control.Monad.Basic -import Mathlib.Control.Random -import Mathlib.Control.SimpSet -import Mathlib.Control.Traversable.Basic -import Mathlib.Control.Traversable.Equiv -import Mathlib.Control.Traversable.Instances -import Mathlib.Control.Traversable.Lemmas -import Mathlib.Control.ULift -import Mathlib.Control.Writer -import Mathlib.Data.Analysis.Filter -import Mathlib.Data.Array.Basic -import Mathlib.Data.Array.Defs -import Mathlib.Data.BinaryHeap -import Mathlib.Data.Bitvec.Core -import Mathlib.Data.Bool.AllAny -import Mathlib.Data.Bool.Basic -import Mathlib.Data.Bool.Count -import Mathlib.Data.Bool.Set -import Mathlib.Data.Bracket -import Mathlib.Data.Bundle -import Mathlib.Data.ByteArray -import Mathlib.Data.Char -import Mathlib.Data.Countable.Basic -import Mathlib.Data.Countable.Defs -import Mathlib.Data.Countable.Small -import Mathlib.Data.DList.Basic -import Mathlib.Data.DList.Instances -import Mathlib.Data.Dfinsupp.Basic -import Mathlib.Data.Dfinsupp.Interval -import Mathlib.Data.Dfinsupp.Lex -import Mathlib.Data.Dfinsupp.Multiset -import Mathlib.Data.Dfinsupp.NeLocus -import Mathlib.Data.Dfinsupp.Order -import Mathlib.Data.ENat.Basic -import Mathlib.Data.ENat.Lattice -import Mathlib.Data.Equiv.Functor -import Mathlib.Data.Erased -import Mathlib.Data.FP.Basic -import Mathlib.Data.Fin.Basic -import Mathlib.Data.Fin.Fin2 -import Mathlib.Data.Fin.Interval -import Mathlib.Data.Fin.SuccPred -import Mathlib.Data.Fin.Tuple.Basic -import Mathlib.Data.Fin.Tuple.BubbleSortInduction -import Mathlib.Data.Fin.Tuple.Monotone -import Mathlib.Data.Fin.Tuple.NatAntidiagonal -import Mathlib.Data.Fin.Tuple.Sort -import Mathlib.Data.Fin.VecNotation -import Mathlib.Data.FinEnum -import Mathlib.Data.Finite.Basic -import Mathlib.Data.Finite.Card -import Mathlib.Data.Finite.Defs -import Mathlib.Data.Finite.Set -import Mathlib.Data.Finmap -import Mathlib.Data.Finset.Basic -import Mathlib.Data.Finset.Card -import Mathlib.Data.Finset.Fin -import Mathlib.Data.Finset.Finsupp -import Mathlib.Data.Finset.Fold -import Mathlib.Data.Finset.Functor -import Mathlib.Data.Finset.Image -import Mathlib.Data.Finset.Lattice -import Mathlib.Data.Finset.LocallyFinite -import Mathlib.Data.Finset.MulAntidiagonal -import Mathlib.Data.Finset.NAry -import Mathlib.Data.Finset.NatAntidiagonal -import Mathlib.Data.Finset.NoncommProd -import Mathlib.Data.Finset.Option -import Mathlib.Data.Finset.Order -import Mathlib.Data.Finset.PImage -import Mathlib.Data.Finset.Pairwise -import Mathlib.Data.Finset.Pi -import Mathlib.Data.Finset.PiInduction -import Mathlib.Data.Finset.Pointwise -import Mathlib.Data.Finset.Powerset -import Mathlib.Data.Finset.Preimage -import Mathlib.Data.Finset.Prod -import Mathlib.Data.Finset.Sigma -import Mathlib.Data.Finset.Slice -import Mathlib.Data.Finset.Sort -import Mathlib.Data.Finset.Sum -import Mathlib.Data.Finsupp.AList -import Mathlib.Data.Finsupp.Antidiagonal -import Mathlib.Data.Finsupp.Basic -import Mathlib.Data.Finsupp.BigOperators -import Mathlib.Data.Finsupp.Defs -import Mathlib.Data.Finsupp.Fin -import Mathlib.Data.Finsupp.Fintype -import Mathlib.Data.Finsupp.Indicator -import Mathlib.Data.Finsupp.Interval -import Mathlib.Data.Finsupp.Lex -import Mathlib.Data.Finsupp.Multiset -import Mathlib.Data.Finsupp.NeLocus -import Mathlib.Data.Finsupp.Order -import Mathlib.Data.Finsupp.Pointwise -import Mathlib.Data.Finsupp.Pwo -import Mathlib.Data.Finsupp.ToDfinsupp -import Mathlib.Data.Fintype.Basic -import Mathlib.Data.Fintype.BigOperators -import Mathlib.Data.Fintype.Card -import Mathlib.Data.Fintype.CardEmbedding -import Mathlib.Data.Fintype.Fin -import Mathlib.Data.Fintype.Lattice -import Mathlib.Data.Fintype.List -import Mathlib.Data.Fintype.Option -import Mathlib.Data.Fintype.Order -import Mathlib.Data.Fintype.Parity -import Mathlib.Data.Fintype.Perm -import Mathlib.Data.Fintype.Pi -import Mathlib.Data.Fintype.Powerset -import Mathlib.Data.Fintype.Prod -import Mathlib.Data.Fintype.Sigma -import Mathlib.Data.Fintype.Small -import Mathlib.Data.Fintype.Sort -import Mathlib.Data.Fintype.Sum -import Mathlib.Data.Fintype.Units -import Mathlib.Data.Fintype.Vector -import Mathlib.Data.FunLike.Basic -import Mathlib.Data.FunLike.Embedding -import Mathlib.Data.FunLike.Equiv -import Mathlib.Data.FunLike.Fintype -import Mathlib.Data.HashMap -import Mathlib.Data.Holor -import Mathlib.Data.Int.AbsoluteValue -import Mathlib.Data.Int.Associated -import Mathlib.Data.Int.Basic -import Mathlib.Data.Int.Bitwise -import Mathlib.Data.Int.Cast.Basic -import Mathlib.Data.Int.Cast.Defs -import Mathlib.Data.Int.Cast.Field -import Mathlib.Data.Int.Cast.Lemmas -import Mathlib.Data.Int.Cast.Prod -import Mathlib.Data.Int.CharZero -import Mathlib.Data.Int.ConditionallyCompleteOrder -import Mathlib.Data.Int.Div -import Mathlib.Data.Int.Dvd.Basic -import Mathlib.Data.Int.Dvd.Pow -import Mathlib.Data.Int.GCD -import Mathlib.Data.Int.Interval -import Mathlib.Data.Int.LeastGreatest -import Mathlib.Data.Int.Lemmas -import Mathlib.Data.Int.Log -import Mathlib.Data.Int.ModEq -import Mathlib.Data.Int.NatPrime -import Mathlib.Data.Int.Order.Basic -import Mathlib.Data.Int.Order.Lemmas -import Mathlib.Data.Int.Order.Units -import Mathlib.Data.Int.Parity -import Mathlib.Data.Int.Range -import Mathlib.Data.Int.Sqrt -import Mathlib.Data.Int.SuccPred -import Mathlib.Data.Int.Units -import Mathlib.Data.KVMap -import Mathlib.Data.LazyList -import Mathlib.Data.LazyList.Basic -import Mathlib.Data.List.AList -import Mathlib.Data.List.Basic -import Mathlib.Data.List.BigOperators.Basic -import Mathlib.Data.List.BigOperators.Lemmas -import Mathlib.Data.List.Card -import Mathlib.Data.List.Chain -import Mathlib.Data.List.Count -import Mathlib.Data.List.Cycle -import Mathlib.Data.List.Dedup -import Mathlib.Data.List.Defs -import Mathlib.Data.List.Destutter -import Mathlib.Data.List.Duplicate -import Mathlib.Data.List.FinRange -import Mathlib.Data.List.Forall2 -import Mathlib.Data.List.Func -import Mathlib.Data.List.Indexes -import Mathlib.Data.List.Infix -import Mathlib.Data.List.Join -import Mathlib.Data.List.Lattice -import Mathlib.Data.List.Lemmas -import Mathlib.Data.List.Lex -import Mathlib.Data.List.MinMax -import Mathlib.Data.List.NatAntidiagonal -import Mathlib.Data.List.Nodup -import Mathlib.Data.List.NodupEquivFin -import Mathlib.Data.List.OfFn -import Mathlib.Data.List.Pairwise -import Mathlib.Data.List.Palindrome -import Mathlib.Data.List.Perm -import Mathlib.Data.List.Permutation -import Mathlib.Data.List.Prime -import Mathlib.Data.List.ProdSigma -import Mathlib.Data.List.Range -import Mathlib.Data.List.Rdrop -import Mathlib.Data.List.Rotate -import Mathlib.Data.List.Sections -import Mathlib.Data.List.Sigma -import Mathlib.Data.List.Sort -import Mathlib.Data.List.Sublists -import Mathlib.Data.List.TFAE -import Mathlib.Data.List.Zip -import Mathlib.Data.Matrix.DMatrix -import Mathlib.Data.Multiset.Antidiagonal -import Mathlib.Data.Multiset.Basic -import Mathlib.Data.Multiset.Bind -import Mathlib.Data.Multiset.Dedup -import Mathlib.Data.Multiset.FinsetOps -import Mathlib.Data.Multiset.Fintype -import Mathlib.Data.Multiset.Fold -import Mathlib.Data.Multiset.Functor -import Mathlib.Data.Multiset.Lattice -import Mathlib.Data.Multiset.LocallyFinite -import Mathlib.Data.Multiset.NatAntidiagonal -import Mathlib.Data.Multiset.Nodup -import Mathlib.Data.Multiset.Pi -import Mathlib.Data.Multiset.Powerset -import Mathlib.Data.Multiset.Range -import Mathlib.Data.Multiset.Sections -import Mathlib.Data.Multiset.Sort -import Mathlib.Data.Multiset.Sum -import Mathlib.Data.Nat.Basic -import Mathlib.Data.Nat.Bits -import Mathlib.Data.Nat.Bitwise -import Mathlib.Data.Nat.Cast.Basic -import Mathlib.Data.Nat.Cast.Defs -import Mathlib.Data.Nat.Cast.Field -import Mathlib.Data.Nat.Cast.Prod -import Mathlib.Data.Nat.Cast.WithTop -import Mathlib.Data.Nat.Choose.Basic -import Mathlib.Data.Nat.Choose.Bounds -import Mathlib.Data.Nat.Choose.Central -import Mathlib.Data.Nat.Choose.Dvd -import Mathlib.Data.Nat.Choose.Sum -import Mathlib.Data.Nat.Count -import Mathlib.Data.Nat.Dist -import Mathlib.Data.Nat.EvenOddRec -import Mathlib.Data.Nat.Factorial.Basic -import Mathlib.Data.Nat.Factorial.BigOperators -import Mathlib.Data.Nat.Factors -import Mathlib.Data.Nat.Fib -import Mathlib.Data.Nat.ForSqrt -import Mathlib.Data.Nat.GCD.Basic -import Mathlib.Data.Nat.GCD.BigOperators -import Mathlib.Data.Nat.Hyperoperation -import Mathlib.Data.Nat.Interval -import Mathlib.Data.Nat.Lattice -import Mathlib.Data.Nat.Log -import Mathlib.Data.Nat.ModEq -import Mathlib.Data.Nat.Order.Basic -import Mathlib.Data.Nat.Order.Lemmas -import Mathlib.Data.Nat.PSub -import Mathlib.Data.Nat.Pairing -import Mathlib.Data.Nat.Parity -import Mathlib.Data.Nat.PartENat -import Mathlib.Data.Nat.Periodic -import Mathlib.Data.Nat.Pow -import Mathlib.Data.Nat.Prime -import Mathlib.Data.Nat.PrimeFin -import Mathlib.Data.Nat.Set -import Mathlib.Data.Nat.Size -import Mathlib.Data.Nat.Sqrt -import Mathlib.Data.Nat.SuccPred -import Mathlib.Data.Nat.Units -import Mathlib.Data.Nat.Upto -import Mathlib.Data.Nat.WithBot -import Mathlib.Data.Num.Basic -import Mathlib.Data.Num.Bitwise -import Mathlib.Data.Opposite -import Mathlib.Data.Option.Basic -import Mathlib.Data.Option.Defs -import Mathlib.Data.Option.NAry -import Mathlib.Data.PEquiv -import Mathlib.Data.PFun -import Mathlib.Data.PFunctor.Multivariate.Basic -import Mathlib.Data.PFunctor.Univariate.Basic -import Mathlib.Data.PFunctor.Univariate.M -import Mathlib.Data.PNat.Basic -import Mathlib.Data.PNat.Defs -import Mathlib.Data.PNat.Factors -import Mathlib.Data.PNat.Find -import Mathlib.Data.PNat.Interval -import Mathlib.Data.PNat.Prime -import Mathlib.Data.PNat.Xgcd -import Mathlib.Data.PSigma.Order -import Mathlib.Data.Part -import Mathlib.Data.Pi.Algebra -import Mathlib.Data.Pi.Interval -import Mathlib.Data.Pi.Lex -import Mathlib.Data.Prod.Basic -import Mathlib.Data.Prod.Lex -import Mathlib.Data.Prod.PProd -import Mathlib.Data.Prod.TProd -import Mathlib.Data.Quot -import Mathlib.Data.Rat.Basic -import Mathlib.Data.Rat.BigOperators -import Mathlib.Data.Rat.Cast -import Mathlib.Data.Rat.Defs -import Mathlib.Data.Rat.Denumerable -import Mathlib.Data.Rat.Encodable -import Mathlib.Data.Rat.Floor -import Mathlib.Data.Rat.Init -import Mathlib.Data.Rat.Lemmas -import Mathlib.Data.Rat.Order -import Mathlib.Data.Rat.Sqrt -import Mathlib.Data.Real.Basic -import Mathlib.Data.Real.CauSeq -import Mathlib.Data.Real.CauSeqCompletion -import Mathlib.Data.Real.Pointwise -import Mathlib.Data.Real.Sign -import Mathlib.Data.Rel -import Mathlib.Data.Semiquot -import Mathlib.Data.Seq.Computation -import Mathlib.Data.Set.Accumulate -import Mathlib.Data.Set.Basic -import Mathlib.Data.Set.BoolIndicator -import Mathlib.Data.Set.Constructions -import Mathlib.Data.Set.Countable -import Mathlib.Data.Set.Enumerate -import Mathlib.Data.Set.Equitable -import Mathlib.Data.Set.Finite -import Mathlib.Data.Set.Function -import Mathlib.Data.Set.Functor -import Mathlib.Data.Set.Image -import Mathlib.Data.Set.Intervals.Basic -import Mathlib.Data.Set.Intervals.Disjoint -import Mathlib.Data.Set.Intervals.Group -import Mathlib.Data.Set.Intervals.Infinite -import Mathlib.Data.Set.Intervals.Instances -import Mathlib.Data.Set.Intervals.IsoIoo -import Mathlib.Data.Set.Intervals.Monoid -import Mathlib.Data.Set.Intervals.Monotone -import Mathlib.Data.Set.Intervals.OrdConnected -import Mathlib.Data.Set.Intervals.OrdConnectedComponent -import Mathlib.Data.Set.Intervals.OrderIso -import Mathlib.Data.Set.Intervals.Pi -import Mathlib.Data.Set.Intervals.ProjIcc -import Mathlib.Data.Set.Intervals.SurjOn -import Mathlib.Data.Set.Intervals.UnorderedInterval -import Mathlib.Data.Set.Intervals.WithBotTop -import Mathlib.Data.Set.Lattice -import Mathlib.Data.Set.MulAntidiagonal -import Mathlib.Data.Set.NAry -import Mathlib.Data.Set.Opposite -import Mathlib.Data.Set.Pairwise -import Mathlib.Data.Set.Pointwise.Basic -import Mathlib.Data.Set.Pointwise.BigOperators -import Mathlib.Data.Set.Pointwise.Finite -import Mathlib.Data.Set.Pointwise.Interval -import Mathlib.Data.Set.Pointwise.Iterate -import Mathlib.Data.Set.Pointwise.ListOfFn -import Mathlib.Data.Set.Pointwise.SMul -import Mathlib.Data.Set.Pointwise.Support -import Mathlib.Data.Set.Prod -import Mathlib.Data.Set.Semiring -import Mathlib.Data.Set.Sigma -import Mathlib.Data.Set.UnionLift -import Mathlib.Data.SetLike.Basic -import Mathlib.Data.SetLike.Fintype -import Mathlib.Data.Setoid.Basic -import Mathlib.Data.Setoid.Partition -import Mathlib.Data.Sigma.Basic -import Mathlib.Data.Sigma.Interval -import Mathlib.Data.Sigma.Lex -import Mathlib.Data.Sigma.Order -import Mathlib.Data.Sign -import Mathlib.Data.Stream.Defs -import Mathlib.Data.Stream.Init -import Mathlib.Data.String.Defs -import Mathlib.Data.String.Lemmas -import Mathlib.Data.Subtype -import Mathlib.Data.Sum.Basic -import Mathlib.Data.Sum.Interval -import Mathlib.Data.Sum.Order -import Mathlib.Data.Sym.Basic -import Mathlib.Data.Sym.Sym2 -import Mathlib.Data.TwoPointing -import Mathlib.Data.TypeVec -import Mathlib.Data.TypeVec.Attr -import Mathlib.Data.UInt -import Mathlib.Data.ULift -import Mathlib.Data.UnionFind -import Mathlib.Data.Vector -import Mathlib.Data.Vector.Basic -import Mathlib.Data.Vector.Mem -import Mathlib.Data.Vector.Zip -import Mathlib.Data.W.Basic -import Mathlib.Data.W.Constructions -import Mathlib.Data.ZMod.Defs -import Mathlib.Deprecated.Group -import Mathlib.Deprecated.Ring -import Mathlib.Deprecated.Subgroup -import Mathlib.Deprecated.Submonoid -import Mathlib.Deprecated.Subring -import Mathlib.Dynamics.FixedPoints.Basic -import Mathlib.Dynamics.FixedPoints.Topology -import Mathlib.Dynamics.Minimal -import Mathlib.Dynamics.PeriodicPts -import Mathlib.GroupTheory.Abelianization -import Mathlib.GroupTheory.Archimedean -import Mathlib.GroupTheory.Commensurable -import Mathlib.GroupTheory.Commutator -import Mathlib.GroupTheory.CommutingProbability -import Mathlib.GroupTheory.Congruence -import Mathlib.GroupTheory.Coset -import Mathlib.GroupTheory.Divisible -import Mathlib.GroupTheory.DoubleCoset -import Mathlib.GroupTheory.EckmannHilton -import Mathlib.GroupTheory.Finiteness -import Mathlib.GroupTheory.FreeGroup -import Mathlib.GroupTheory.GroupAction.Basic -import Mathlib.GroupTheory.GroupAction.BigOperators -import Mathlib.GroupTheory.GroupAction.ConjAct -import Mathlib.GroupTheory.GroupAction.Defs -import Mathlib.GroupTheory.GroupAction.Embedding -import Mathlib.GroupTheory.GroupAction.FixingSubgroup -import Mathlib.GroupTheory.GroupAction.Group -import Mathlib.GroupTheory.GroupAction.Opposite -import Mathlib.GroupTheory.GroupAction.Option -import Mathlib.GroupTheory.GroupAction.Pi -import Mathlib.GroupTheory.GroupAction.Prod -import Mathlib.GroupTheory.GroupAction.Quotient -import Mathlib.GroupTheory.GroupAction.Sigma -import Mathlib.GroupTheory.GroupAction.SubMulAction -import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise -import Mathlib.GroupTheory.GroupAction.Sum -import Mathlib.GroupTheory.GroupAction.Support -import Mathlib.GroupTheory.GroupAction.Units -import Mathlib.GroupTheory.Index -import Mathlib.GroupTheory.IsFreeGroup -import Mathlib.GroupTheory.MonoidLocalization -import Mathlib.GroupTheory.Perm.Basic -import Mathlib.GroupTheory.Perm.List -import Mathlib.GroupTheory.Perm.Subgroup -import Mathlib.GroupTheory.Perm.Support -import Mathlib.GroupTheory.Perm.ViaEmbedding -import Mathlib.GroupTheory.PresentedGroup -import Mathlib.GroupTheory.QuotientGroup -import Mathlib.GroupTheory.SemidirectProduct -import Mathlib.GroupTheory.Subgroup.Actions -import Mathlib.GroupTheory.Subgroup.Basic -import Mathlib.GroupTheory.Subgroup.Finite -import Mathlib.GroupTheory.Subgroup.MulOpposite -import Mathlib.GroupTheory.Subgroup.Pointwise -import Mathlib.GroupTheory.Subgroup.Saturated -import Mathlib.GroupTheory.Subgroup.Simple -import Mathlib.GroupTheory.Subgroup.Zpowers -import Mathlib.GroupTheory.Submonoid.Basic -import Mathlib.GroupTheory.Submonoid.Center -import Mathlib.GroupTheory.Submonoid.Centralizer -import Mathlib.GroupTheory.Submonoid.Inverses -import Mathlib.GroupTheory.Submonoid.Membership -import Mathlib.GroupTheory.Submonoid.Operations -import Mathlib.GroupTheory.Submonoid.Pointwise -import Mathlib.GroupTheory.Subsemigroup.Basic -import Mathlib.GroupTheory.Subsemigroup.Center -import Mathlib.GroupTheory.Subsemigroup.Centralizer -import Mathlib.GroupTheory.Subsemigroup.Membership -import Mathlib.GroupTheory.Subsemigroup.Operations -import Mathlib.Init.Algebra.Classes -import Mathlib.Init.Algebra.Functions -import Mathlib.Init.Algebra.Order -import Mathlib.Init.Align -import Mathlib.Init.CcLemmas -import Mathlib.Init.Classes.Order -import Mathlib.Init.Classical -import Mathlib.Init.Control.Combinators -import Mathlib.Init.Core -import Mathlib.Init.Data.Bool.Basic -import Mathlib.Init.Data.Bool.Lemmas -import Mathlib.Init.Data.Fin.Basic -import Mathlib.Init.Data.Int.Basic -import Mathlib.Init.Data.Int.Bitwise -import Mathlib.Init.Data.Int.DivMod -import Mathlib.Init.Data.Int.Lemmas -import Mathlib.Init.Data.Int.Order -import Mathlib.Init.Data.List.Basic -import Mathlib.Init.Data.List.Instances -import Mathlib.Init.Data.List.Lemmas -import Mathlib.Init.Data.Nat.Basic -import Mathlib.Init.Data.Nat.Bitwise -import Mathlib.Init.Data.Nat.Div -import Mathlib.Init.Data.Nat.GCD -import Mathlib.Init.Data.Nat.Lemmas -import Mathlib.Init.Data.Nat.Notation -import Mathlib.Init.Data.Option.Basic -import Mathlib.Init.Data.Option.Init.Lemmas -import Mathlib.Init.Data.Option.Lemmas -import Mathlib.Init.Data.Ordering.Basic -import Mathlib.Init.Data.Prod -import Mathlib.Init.Data.Quot -import Mathlib.Init.Data.Rat.Basic -import Mathlib.Init.Data.Sigma.Basic -import Mathlib.Init.Data.Subtype.Basic -import Mathlib.Init.Function -import Mathlib.Init.Logic -import Mathlib.Init.Meta.WellFoundedTactics -import Mathlib.Init.Propext -import Mathlib.Init.Quot -import Mathlib.Init.Set -import Mathlib.Init.ZeroOne -import Mathlib.Lean.EnvExtension -import Mathlib.Lean.Exception -import Mathlib.Lean.Expr -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.Expr.ReplaceRec -import Mathlib.Lean.Expr.Traverse -import Mathlib.Lean.LocalContext -import Mathlib.Lean.Message -import Mathlib.Lean.Meta -import Mathlib.Lean.Meta.Simp -import Mathlib.LinearAlgebra.AffineSpace.Basic -import Mathlib.LinearAlgebra.Basic -import Mathlib.LinearAlgebra.GeneralLinearGroup -import Mathlib.LinearAlgebra.Pi -import Mathlib.LinearAlgebra.Quotient -import Mathlib.LinearAlgebra.Span -import Mathlib.Logic.Basic -import Mathlib.Logic.Denumerable -import Mathlib.Logic.Embedding.Basic -import Mathlib.Logic.Embedding.Set -import Mathlib.Logic.Encodable.Basic -import Mathlib.Logic.Encodable.Lattice -import Mathlib.Logic.Equiv.Basic -import Mathlib.Logic.Equiv.Defs -import Mathlib.Logic.Equiv.Embedding -import Mathlib.Logic.Equiv.Fin -import Mathlib.Logic.Equiv.List -import Mathlib.Logic.Equiv.LocalEquiv -import Mathlib.Logic.Equiv.MfldSimpsAttr -import Mathlib.Logic.Equiv.Nat -import Mathlib.Logic.Equiv.Option -import Mathlib.Logic.Equiv.Set -import Mathlib.Logic.Function.Basic -import Mathlib.Logic.Function.Conjugate -import Mathlib.Logic.Function.Iterate -import Mathlib.Logic.IsEmpty -import Mathlib.Logic.Lemmas -import Mathlib.Logic.Nonempty -import Mathlib.Logic.Nontrivial -import Mathlib.Logic.Pairwise -import Mathlib.Logic.Relation -import Mathlib.Logic.Relator -import Mathlib.Logic.Small.Basic -import Mathlib.Logic.Small.List -import Mathlib.Logic.Unique -import Mathlib.Mathport.Attributes -import Mathlib.Mathport.Notation -import Mathlib.Mathport.Rename -import Mathlib.Mathport.Syntax -import Mathlib.MeasureTheory.MeasurableSpace -import Mathlib.MeasureTheory.MeasurableSpaceDef -import Mathlib.MeasureTheory.PiSystem -import Mathlib.NumberTheory.ADEInequality -import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue -import Mathlib.NumberTheory.Divisors -import Mathlib.NumberTheory.FrobeniusNumber -import Mathlib.NumberTheory.Primorial -import Mathlib.Order.Antichain -import Mathlib.Order.Antisymmetrization -import Mathlib.Order.Atoms -import Mathlib.Order.Atoms.Finite -import Mathlib.Order.Basic -import Mathlib.Order.BooleanAlgebra -import Mathlib.Order.Bounded -import Mathlib.Order.BoundedOrder -import Mathlib.Order.Bounds.Basic -import Mathlib.Order.Bounds.OrderIso -import Mathlib.Order.Chain -import Mathlib.Order.Circular -import Mathlib.Order.Closure -import Mathlib.Order.CompactlyGenerated -import Mathlib.Order.Compare -import Mathlib.Order.CompleteBooleanAlgebra -import Mathlib.Order.CompleteLattice -import Mathlib.Order.CompleteLatticeIntervals -import Mathlib.Order.Concept -import Mathlib.Order.ConditionallyCompleteLattice.Basic -import Mathlib.Order.ConditionallyCompleteLattice.Finset -import Mathlib.Order.ConditionallyCompleteLattice.Group -import Mathlib.Order.Copy -import Mathlib.Order.CountableDenseLinearOrder -import Mathlib.Order.Cover -import Mathlib.Order.Directed -import Mathlib.Order.Disjoint -import Mathlib.Order.Disjointed -import Mathlib.Order.Extension.Linear -import Mathlib.Order.Extension.Well -import Mathlib.Order.Filter.Archimedean -import Mathlib.Order.Filter.AtTopBot -import Mathlib.Order.Filter.Bases -import Mathlib.Order.Filter.Basic -import Mathlib.Order.Filter.Cofinite -import Mathlib.Order.Filter.CountableInter -import Mathlib.Order.Filter.Curry -import Mathlib.Order.Filter.Extr -import Mathlib.Order.Filter.Germ -import Mathlib.Order.Filter.IndicatorFunction -import Mathlib.Order.Filter.Interval -import Mathlib.Order.Filter.Lift -import Mathlib.Order.Filter.ModEq -import Mathlib.Order.Filter.NAry -import Mathlib.Order.Filter.Partial -import Mathlib.Order.Filter.Pi -import Mathlib.Order.Filter.Pointwise -import Mathlib.Order.Filter.Prod -import Mathlib.Order.Filter.SmallSets -import Mathlib.Order.Filter.Ultrafilter -import Mathlib.Order.FixedPoints -import Mathlib.Order.GaloisConnection -import Mathlib.Order.GameAdd -import Mathlib.Order.Grade -import Mathlib.Order.Heyting.Basic -import Mathlib.Order.Heyting.Boundary -import Mathlib.Order.Heyting.Hom -import Mathlib.Order.Heyting.Regular -import Mathlib.Order.Hom.Basic -import Mathlib.Order.Hom.Bounded -import Mathlib.Order.Hom.CompleteLattice -import Mathlib.Order.Hom.Lattice -import Mathlib.Order.Hom.Order -import Mathlib.Order.Hom.Set -import Mathlib.Order.Ideal -import Mathlib.Order.InitialSeg -import Mathlib.Order.Iterate -import Mathlib.Order.Lattice -import Mathlib.Order.LatticeIntervals -import Mathlib.Order.LiminfLimsup -import Mathlib.Order.LocallyFinite -import Mathlib.Order.Max -import Mathlib.Order.MinMax -import Mathlib.Order.Minimal -import Mathlib.Order.ModularLattice -import Mathlib.Order.Monotone.Basic -import Mathlib.Order.Monotone.Extension -import Mathlib.Order.Monotone.Monovary -import Mathlib.Order.Monotone.Odd -import Mathlib.Order.Monotone.Union -import Mathlib.Order.OmegaCompletePartialOrder -import Mathlib.Order.OrdContinuous -import Mathlib.Order.OrderIsoNat -import Mathlib.Order.PFilter -import Mathlib.Order.PartialSups -import Mathlib.Order.Partition.Equipartition -import Mathlib.Order.Partition.Finpartition -import Mathlib.Order.PrimeIdeal -import Mathlib.Order.PropInstances -import Mathlib.Order.RelClasses -import Mathlib.Order.RelIso.Basic -import Mathlib.Order.RelIso.Group -import Mathlib.Order.RelIso.Set -import Mathlib.Order.SemiconjSup -import Mathlib.Order.SuccPred.Basic -import Mathlib.Order.SuccPred.IntervalSucc -import Mathlib.Order.SuccPred.Limit -import Mathlib.Order.SuccPred.LinearLocallyFinite -import Mathlib.Order.SuccPred.Relation -import Mathlib.Order.SupIndep -import Mathlib.Order.SymmDiff -import Mathlib.Order.Synonym -import Mathlib.Order.UpperLower.Basic -import Mathlib.Order.UpperLower.Hom -import Mathlib.Order.WellFounded -import Mathlib.Order.WellFoundedSet -import Mathlib.Order.WithBot -import Mathlib.Order.Zorn -import Mathlib.Order.ZornAtoms -import Mathlib.RingTheory.Congruence -import Mathlib.RingTheory.Coprime.Basic -import Mathlib.RingTheory.Coprime.Lemmas -import Mathlib.RingTheory.Fintype -import Mathlib.RingTheory.NonZeroDivisors -import Mathlib.RingTheory.OreLocalization.Basic -import Mathlib.RingTheory.OreLocalization.OreSet -import Mathlib.RingTheory.Prime -import Mathlib.RingTheory.RingInvo -import Mathlib.RingTheory.Subring.Basic -import Mathlib.RingTheory.Subsemiring.Basic -import Mathlib.RingTheory.Subsemiring.Pointwise -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.SetTheory.Cardinal.Finite -import Mathlib.SetTheory.Cardinal.SchroederBernstein -import Mathlib.SetTheory.Lists -import Mathlib.SetTheory.Ordinal.Arithmetic -import Mathlib.SetTheory.Ordinal.Basic -import Mathlib.SetTheory.Ordinal.NaturalOps -import Mathlib.SetTheory.Ordinal.Topology -import Mathlib.Tactic.Abel -import Mathlib.Tactic.Alias -import Mathlib.Tactic.ApplyFun -import Mathlib.Tactic.ApplyWith -import Mathlib.Tactic.Basic -import Mathlib.Tactic.ByContra -import Mathlib.Tactic.Cache -import Mathlib.Tactic.Cases -import Mathlib.Tactic.CasesM -import Mathlib.Tactic.Choose -import Mathlib.Tactic.Classical -import Mathlib.Tactic.Clear! -import Mathlib.Tactic.ClearExcept -import Mathlib.Tactic.Clear_ -import Mathlib.Tactic.Coe -import Mathlib.Tactic.Constructor -import Mathlib.Tactic.Continuity -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Conv -import Mathlib.Tactic.Convert -import Mathlib.Tactic.Core -import Mathlib.Tactic.Existsi -import Mathlib.Tactic.Expect -import Mathlib.Tactic.FailIfNoProgress -import Mathlib.Tactic.FieldSimp -import Mathlib.Tactic.FinCases -import Mathlib.Tactic.Find -import Mathlib.Tactic.GeneralizeProofs -import Mathlib.Tactic.Group -import Mathlib.Tactic.GuardGoalNums -import Mathlib.Tactic.GuardHypNums -import Mathlib.Tactic.Have -import Mathlib.Tactic.HelpCmd -import Mathlib.Tactic.InferParam -import Mathlib.Tactic.Inhabit -import Mathlib.Tactic.IntervalCases -import Mathlib.Tactic.IrreducibleDef -import Mathlib.Tactic.LabelAttr -import Mathlib.Tactic.LeftRight -import Mathlib.Tactic.LibrarySearch -import Mathlib.Tactic.Lift -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.Linarith.Datatypes -import Mathlib.Tactic.Linarith.Elimination -import Mathlib.Tactic.Linarith.Frontend -import Mathlib.Tactic.Linarith.Lemmas -import Mathlib.Tactic.Linarith.Parsing -import Mathlib.Tactic.Linarith.Preprocessing -import Mathlib.Tactic.Linarith.Verification -import Mathlib.Tactic.LinearCombination -import Mathlib.Tactic.MkIffOfInductiveProp -import Mathlib.Tactic.ModCases -import Mathlib.Tactic.Monotonicity -import Mathlib.Tactic.Monotonicity.Attr -import Mathlib.Tactic.Monotonicity.Basic -import Mathlib.Tactic.Monotonicity.Lemmas -import Mathlib.Tactic.Nontriviality -import Mathlib.Tactic.Nontriviality.Core -import Mathlib.Tactic.NormCast -import Mathlib.Tactic.NormCast.Tactic -import Mathlib.Tactic.NormNum -import Mathlib.Tactic.NormNum.Basic -import Mathlib.Tactic.NormNum.Core -import Mathlib.Tactic.NthRewrite -import Mathlib.Tactic.PermuteGoals -import Mathlib.Tactic.Polyrith -import Mathlib.Tactic.Positivity -import Mathlib.Tactic.Positivity.Basic -import Mathlib.Tactic.Positivity.Core -import Mathlib.Tactic.PrintPrefix -import Mathlib.Tactic.PushNeg -import Mathlib.Tactic.Qify -import Mathlib.Tactic.Qify.Attr -import Mathlib.Tactic.RSuffices -import Mathlib.Tactic.Reassoc -import Mathlib.Tactic.Recover -import Mathlib.Tactic.Relation.Rfl -import Mathlib.Tactic.Relation.Symm -import Mathlib.Tactic.Relation.Trans -import Mathlib.Tactic.Rename -import Mathlib.Tactic.RenameBVar -import Mathlib.Tactic.Replace -import Mathlib.Tactic.RestateAxiom -import Mathlib.Tactic.Ring -import Mathlib.Tactic.Ring.Basic -import Mathlib.Tactic.Ring.RingNF -import Mathlib.Tactic.RunCmd -import Mathlib.Tactic.Sat.FromLRAT -import Mathlib.Tactic.ScopedNS -import Mathlib.Tactic.Set -import Mathlib.Tactic.SimpIntro -import Mathlib.Tactic.SimpRw -import Mathlib.Tactic.Simps.Basic -import Mathlib.Tactic.Simps.NotationClass -import Mathlib.Tactic.Slice -import Mathlib.Tactic.SolveByElim -import Mathlib.Tactic.SplitIfs -import Mathlib.Tactic.Spread -import Mathlib.Tactic.Substs -import Mathlib.Tactic.SudoSetOption -import Mathlib.Tactic.SwapVar -import Mathlib.Tactic.Tauto -import Mathlib.Tactic.ToAdditive -import Mathlib.Tactic.Trace -import Mathlib.Tactic.TypeCheck -import Mathlib.Tactic.UnsetOption -import Mathlib.Tactic.Use -import Mathlib.Tactic.WLOG -import Mathlib.Tactic.Zify -import Mathlib.Tactic.Zify.Attr -import Mathlib.Testing.SlimCheck.Gen -import Mathlib.Testing.SlimCheck.Sampleable -import Mathlib.Testing.SlimCheck.Testable -import Mathlib.Topology.Alexandroff -import Mathlib.Topology.Algebra.ConstMulAction -import Mathlib.Topology.Algebra.Constructions -import Mathlib.Topology.Algebra.GroupWithZero -import Mathlib.Topology.Algebra.Monoid -import Mathlib.Topology.Algebra.MulAction -import Mathlib.Topology.Algebra.Order.Archimedean -import Mathlib.Topology.Algebra.Order.Compact -import Mathlib.Topology.Algebra.Order.ExtendFrom -import Mathlib.Topology.Algebra.Order.ExtrClosure -import Mathlib.Topology.Algebra.Order.Filter -import Mathlib.Topology.Algebra.Order.IntermediateValue -import Mathlib.Topology.Algebra.Order.LeftRight -import Mathlib.Topology.Algebra.Order.LeftRightLim -import Mathlib.Topology.Algebra.Order.LiminfLimsup -import Mathlib.Topology.Algebra.Order.MonotoneContinuity -import Mathlib.Topology.Algebra.Order.MonotoneConvergence -import Mathlib.Topology.Algebra.Order.ProjIcc -import Mathlib.Topology.Algebra.Order.T5 -import Mathlib.Topology.Algebra.Semigroup -import Mathlib.Topology.Algebra.Star -import Mathlib.Topology.Bases -import Mathlib.Topology.Basic -import Mathlib.Topology.Bornology.Basic -import Mathlib.Topology.Bornology.Constructions -import Mathlib.Topology.Bornology.Hom -import Mathlib.Topology.CompactOpen -import Mathlib.Topology.Connected -import Mathlib.Topology.Constructions -import Mathlib.Topology.ContinuousFunction.Basic -import Mathlib.Topology.ContinuousFunction.CocompactMap -import Mathlib.Topology.ContinuousFunction.T0Sierpinski -import Mathlib.Topology.ContinuousOn -import Mathlib.Topology.DenseEmbedding -import Mathlib.Topology.DiscreteQuotient -import Mathlib.Topology.ExtendFrom -import Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle -import Mathlib.Topology.Filter -import Mathlib.Topology.GDelta -import Mathlib.Topology.Hom.Open -import Mathlib.Topology.Homeomorph -import Mathlib.Topology.Inseparable -import Mathlib.Topology.Instances.Sign -import Mathlib.Topology.List -import Mathlib.Topology.LocalExtr -import Mathlib.Topology.LocalHomeomorph -import Mathlib.Topology.LocallyConstant.Basic -import Mathlib.Topology.LocallyFinite -import Mathlib.Topology.Maps -import Mathlib.Topology.NhdsSet -import Mathlib.Topology.NoetherianSpace -import Mathlib.Topology.OmegaCompletePartialOrder -import Mathlib.Topology.Order -import Mathlib.Topology.Order.Basic -import Mathlib.Topology.Order.Hom.Basic -import Mathlib.Topology.Order.Lattice -import Mathlib.Topology.Order.LowerTopology -import Mathlib.Topology.Order.Priestley -import Mathlib.Topology.Paracompact -import Mathlib.Topology.Partial -import Mathlib.Topology.Perfect -import Mathlib.Topology.QuasiSeparated -import Mathlib.Topology.Separation -import Mathlib.Topology.Sets.Closeds -import Mathlib.Topology.Sets.Compacts -import Mathlib.Topology.Sets.Opens -import Mathlib.Topology.Sets.Order -import Mathlib.Topology.ShrinkingLemma -import Mathlib.Topology.Sober -import Mathlib.Topology.Spectral.Hom -import Mathlib.Topology.StoneCech -import Mathlib.Topology.SubsetProperties -import Mathlib.Topology.Support -import Mathlib.Topology.UniformSpace.AbsoluteValue -import Mathlib.Topology.UniformSpace.AbstractCompletion -import Mathlib.Topology.UniformSpace.Basic -import Mathlib.Topology.UniformSpace.Cauchy -import Mathlib.Topology.UniformSpace.CompactConvergence -import Mathlib.Topology.UniformSpace.CompleteSeparated -import Mathlib.Topology.UniformSpace.Completion -import Mathlib.Topology.UniformSpace.Equiv -import Mathlib.Topology.UniformSpace.Pi -import Mathlib.Topology.UniformSpace.Separation -import Mathlib.Topology.UniformSpace.UniformConvergence -import Mathlib.Topology.UniformSpace.UniformEmbedding -import Mathlib.Util.AssertNoSorry -import Mathlib.Util.AtomM -import Mathlib.Util.Export -import Mathlib.Util.IncludeStr -import Mathlib.Util.MemoFix -import Mathlib.Util.Simp -import Mathlib.Util.Syntax -import Mathlib.Util.SynthesizeUsing -import Mathlib.Util.Tactic -import Mathlib.Util.Time -import Mathlib.Util.WhatsNew -import Mathlib.Util.WithWeakNamespace From eb6a39ef03674aaebea4c8bda40b5ba034d212a6 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 11:20:11 -0500 Subject: [PATCH 6/9] fix errors; lint --- .../CategoryTheory/IsomorphismClasses.lean | 27 +++++++++++++------ 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/Mathlib/CategoryTheory/IsomorphismClasses.lean b/Mathlib/CategoryTheory/IsomorphismClasses.lean index 54b851141ac5f..de9d49621d3bf 100644 --- a/Mathlib/CategoryTheory/IsomorphismClasses.lean +++ b/Mathlib/CategoryTheory/IsomorphismClasses.lean @@ -15,7 +15,7 @@ import Mathlib.CategoryTheory.Types /-! # Objects of a category up to an isomorphism -`is_isomorphic X Y := nonempty (X ≅ Y)` is an equivalence relation on the objects of a category. +`IsIsomorphic X Y := Nonempty (X ≅ Y)` is an equivalence relation on the objects of a category. The quotient with respect to this relation defines a functor from our category to `Type`. -/ @@ -36,18 +36,31 @@ variable (C) /-- `is_isomorphic` defines a setoid. -/ def isIsomorphicSetoid : Setoid C where - R := IsIsomorphic - iseqv := ⟨fun X => ⟨Iso.refl X⟩, fun X Y ⟨α⟩ => ⟨α.symm⟩, fun X Y Z ⟨α⟩ ⟨β⟩ => ⟨α.trans β⟩⟩ + r := IsIsomorphic + iseqv := ⟨fun X => ⟨Iso.refl X⟩, fun ⟨α⟩ => ⟨α.symm⟩, fun ⟨α⟩ ⟨β⟩ => ⟨α.trans β⟩⟩ #align category_theory.is_isomorphic_setoid CategoryTheory.isIsomorphicSetoid end Category /-- The functor that sends each category to the quotient space of its objects up to an isomorphism. -/ -def isomorphismClasses : Cat.{v, u} ⥤ Type u - where +def isomorphismClasses : Cat.{v, u} ⥤ Type u where obj C := Quotient (isIsomorphicSetoid C.α) - map C D F := Quot.map F.obj fun X Y ⟨f⟩ => ⟨F.mapIso f⟩ + map {C} {D} F := Quot.map F.obj fun X Y ⟨f⟩ => ⟨F.mapIso f⟩ + map_id {C} := by -- Porting note: this used to be `tidy` + dsimp; apply funext; intro x + apply x.recOn -- Porting note: `induction x` not working yet + · intro _ _ p + simp only [types_id_apply] + · intro _ + rfl + map_comp {C} {D} {E} f g := by -- Porting note(s): idem + dsimp; apply funext; intro x + apply x.recOn + · intro _ _ _ + simp only [types_id_apply] + · intro _ + rfl #align category_theory.isomorphism_classes CategoryTheory.isomorphismClasses theorem Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X Y : C} : @@ -55,7 +68,5 @@ theorem Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X (Groupoid.isoEquivHom X Y).nonempty_congr #align category_theory.groupoid.is_isomorphic_iff_nonempty_hom CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom --- PROJECT: define `skeletal`, and show every category is equivalent to a skeletal category, --- using the axiom of choice to pick a representative of every isomorphism class. end CategoryTheory From f4bbf9e9431e0a844757552fc72e85ae9aa6a78a Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 11:28:03 -0500 Subject: [PATCH 7/9] fix borked import file for real --- Mathlib.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib.lean b/Mathlib.lean index 358c67d94da41..85106bb191c40 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -97,6 +97,7 @@ import Mathlib.Algebra.Homology.ComplexShape import Mathlib.Algebra.IndicatorFunction import Mathlib.Algebra.Invertible import Mathlib.Algebra.IsPrimePow +import Mathlib.Algebra.Module.Algebra import Mathlib.Algebra.Module.Basic import Mathlib.Algebra.Module.BigOperators import Mathlib.Algebra.Module.Equiv @@ -264,6 +265,7 @@ import Mathlib.CategoryTheory.Sigma.Basic import Mathlib.CategoryTheory.Thin import Mathlib.CategoryTheory.Types import Mathlib.CategoryTheory.Whiskering +import Mathlib.CategoryTheory.Yoneda import Mathlib.Combinatorics.Additive.Energy import Mathlib.Combinatorics.Additive.RuzsaCovering import Mathlib.Combinatorics.Colex @@ -571,6 +573,8 @@ import Mathlib.Data.Option.NAry import Mathlib.Data.PEquiv import Mathlib.Data.PFun import Mathlib.Data.PFunctor.Multivariate.Basic +import Mathlib.Data.PFunctor.Multivariate.M +import Mathlib.Data.PFunctor.Multivariate.W import Mathlib.Data.PFunctor.Univariate.Basic import Mathlib.Data.PFunctor.Univariate.M import Mathlib.Data.PNat.Basic @@ -589,6 +593,7 @@ import Mathlib.Data.Prod.Basic import Mathlib.Data.Prod.Lex import Mathlib.Data.Prod.PProd import Mathlib.Data.Prod.TProd +import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Data.Quot import Mathlib.Data.Rat.Basic import Mathlib.Data.Rat.BigOperators @@ -604,6 +609,7 @@ import Mathlib.Data.Rat.Sqrt import Mathlib.Data.Real.Basic import Mathlib.Data.Real.CauSeq import Mathlib.Data.Real.CauSeqCompletion +import Mathlib.Data.Real.NNReal import Mathlib.Data.Real.Pointwise import Mathlib.Data.Real.Sign import Mathlib.Data.Rel @@ -892,6 +898,7 @@ import Mathlib.Order.Filter.Cofinite import Mathlib.Order.Filter.CountableInter import Mathlib.Order.Filter.Curry import Mathlib.Order.Filter.Extr +import Mathlib.Order.Filter.FilterProduct import Mathlib.Order.Filter.Germ import Mathlib.Order.Filter.IndicatorFunction import Mathlib.Order.Filter.Interval @@ -981,6 +988,7 @@ import Mathlib.SetTheory.Cardinal.SchroederBernstein import Mathlib.SetTheory.Lists import Mathlib.SetTheory.Ordinal.Arithmetic import Mathlib.SetTheory.Ordinal.Basic +import Mathlib.SetTheory.Ordinal.Exponential import Mathlib.SetTheory.Ordinal.NaturalOps import Mathlib.SetTheory.Ordinal.Topology import Mathlib.Tactic.Abel @@ -1139,6 +1147,7 @@ import Mathlib.Topology.Hom.Open import Mathlib.Topology.Homeomorph import Mathlib.Topology.Inseparable import Mathlib.Topology.Instances.Sign +import Mathlib.Topology.IsLocallyHomeomorph import Mathlib.Topology.List import Mathlib.Topology.LocalExtr import Mathlib.Topology.LocalHomeomorph From 658c05bcd3e25fba0b90a3d871a6d13e5e0496a8 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Mon, 20 Feb 2023 11:33:14 -0500 Subject: [PATCH 8/9] fix borked import file MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 3rd time = 🧿? --- Mathlib.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib.lean b/Mathlib.lean index 85106bb191c40..70c113f8041e1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -509,6 +509,7 @@ import Mathlib.Data.Multiset.FinsetOps import Mathlib.Data.Multiset.Fintype import Mathlib.Data.Multiset.Fold import Mathlib.Data.Multiset.Functor +import Mathlib.Data.Multiset.Interval import Mathlib.Data.Multiset.Lattice import Mathlib.Data.Multiset.LocallyFinite import Mathlib.Data.Multiset.NatAntidiagonal @@ -856,6 +857,7 @@ import Mathlib.MeasureTheory.MeasurableSpace import Mathlib.MeasureTheory.MeasurableSpaceDef import Mathlib.MeasureTheory.PiSystem import Mathlib.NumberTheory.ADEInequality +import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue import Mathlib.NumberTheory.Divisors import Mathlib.NumberTheory.FrobeniusNumber From 97da3eeae45ca1433a4436a7f96e5ec2485f8515 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Tue, 21 Feb 2023 22:38:49 -0500 Subject: [PATCH 9/9] add updated discrete cat --- Mathlib/CategoryTheory/DiscreteCategory.lean | 61 ++++++-------------- 1 file changed, 17 insertions(+), 44 deletions(-) diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean index cac60eb13ddee..14cc5ef7c9f13 100644 --- a/Mathlib/CategoryTheory/DiscreteCategory.lean +++ b/Mathlib/CategoryTheory/DiscreteCategory.lean @@ -107,22 +107,15 @@ instance [Subsingleton α] : Subsingleton (Discrete α) := ext apply Subsingleton.elim⟩ -/- ./././Mathport/Syntax/Translate/Expr.lean:334:4: warning: unsupported (TODO): `[tacs] -/ -/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/ ---unsafe def _root_.tactic.discrete_cases : tactic Unit := --- sorry ---#align tactic.discrete_cases tactic.discrete_cases - - ---run_cmd --- add_interactive [`` tactic.discrete_cases] +/- +Porting note: It seems that `aesop` currently has no way to add lemmas locally. ---attribute [local tidy] tactic.discrete_cases ---`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]] +attribute [local tidy] tactic.discrete_cases +`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), PLift _]] +-/ ---macro (name := discrete_cases) "discrete_cases" : tactic => --- `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _) /- Porting note: rewrote `discrete_cases` tactic -/ +/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/ macro "discrete_cases": tactic => `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _) @@ -152,7 +145,7 @@ protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y := exact h) #align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso -/-- A variant of `eq_to_hom` that lifts terms to the discrete category. -/ +/-- A variant of `eqToHom` that lifts terms to the discrete category. -/ abbrev eqToHom' {a b : α} (h : a = b) : Discrete.mk a ⟶ Discrete.mk b := Discrete.eqToHom h #align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom' @@ -172,10 +165,7 @@ variable {C : Type u₂} [Category.{v₂} C] instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f := ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩ -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ -/-- Any function `I → C` gives a functor `Discrete I ⥤ C`. --/ +/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/ def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where obj := F ∘ Discrete.as @@ -208,8 +198,6 @@ def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat) #align category_theory.discrete.functor_comp CategoryTheory.Discrete.functorComp -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ /-- For functors out of a discrete category, a natural transformation is just a collection of maps, as the naturality squares are trivial. @@ -218,24 +206,20 @@ as the naturality squares are trivial. def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G where app := f - naturality {X Y} g := by - rcases g with ⟨⟨g⟩⟩ + naturality := fun {X Y} ⟨⟨g⟩⟩ => by discrete_cases rcases g change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _) simp #align category_theory.discrete.nat_trans CategoryTheory.Discrete.natTrans -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ /-- For functors out of a discrete category, a natural isomorphism is just a collection of isomorphisms, as the naturality squares are trivial. -/ @[simps!] def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G := - NatIso.ofComponents f fun g => by - rcases g with ⟨⟨g⟩⟩ + NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by discrete_cases rcases g change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _) @@ -247,8 +231,6 @@ theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discret (i : Discrete I) : (Discrete.natIso f).app i = f i := by aesop_cat #align category_theory.discrete.nat_iso_app CategoryTheory.Discrete.natIso_app -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ /-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to `discrete.functor (F.obj)`. -/ @[simp] @@ -263,11 +245,7 @@ def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : natIso fun _ => Iso.refl _ #align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ -/-- We can promote a type-level `equiv` to +/-- We can promote a type-level `Equiv` to an equivalence between the corresponding `discrete` categories. -/ @[simps] @@ -289,7 +267,7 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D simp) #align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence -/-- We can convert an equivalence of `discrete` categories to a type-level `equiv`. -/ +/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/ @[simps] def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β where @@ -307,27 +285,23 @@ variable {J : Type v₁} open Opposite -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported -\ non-interactive tactic tactic.op_induction' -/ -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported -\ tactic `discrete_cases #[] -/ /-- A discrete category is equivalent to its opposite category. -/ @[simps! functor_obj_as inverse_obj] protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α := let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x) Equivalence.mk F.leftOp F - (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _) - <| fun {X Y} f => by + (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _) <| fun {X Y} ⟨⟨f⟩⟩ => by induction X using Opposite.rec induction Y using Opposite.rec - rcases f with ⟨⟨f⟩⟩ discrete_cases rcases f aesop_cat) (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _) + /- + Porting note: + The following is what was generated by mathport: + refine' Equivalence.mk (F.leftOp) F _ (Discrete.natIso fun X => @@ -361,4 +335,3 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F end Discrete end CategoryTheory -