automated fixes

Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
leanprover-community · Feb 19, 2023 · 64556c5 · 64556c5
1 parent e14a0f5
commit 64556c5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -224,6 +224,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

diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean
@@ -8,10 +8,10 @@ Authors: Yury Kudryashov
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.ConcreteCategory.Bundled
-import Mathbin.CategoryTheory.DiscreteCategory
-import Mathbin.CategoryTheory.Types
-import Mathbin.CategoryTheory.Bicategory.Strict
+import Mathlib.CategoryTheory.ConcreteCategory.Bundled
+import Mathlib.CategoryTheory.DiscreteCategory
+import Mathlib.CategoryTheory.Types
+import Mathlib.CategoryTheory.Bicategory.Strict
 
 /-!
 # Category of categories