automated fixes

Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
leanprover-community · Feb 14, 2023 · e2cfafa · e2cfafa
1 parent 466cb9f
commit e2cfafa
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -235,6 +235,7 @@ import Mathlib.CategoryTheory.Functor.Default
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.InvIsos
+import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans

diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean
@@ -8,11 +8,11 @@ Authors: Reid Barton, Scott Morrison, David Wärn
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.FullSubcategory
-import Mathbin.CategoryTheory.Products.Basic
-import Mathbin.CategoryTheory.Pi.Basic
-import Mathbin.CategoryTheory.Category.Basic
-import Mathbin.Combinatorics.Quiver.ConnectedComponent
+import Mathlib.CategoryTheory.FullSubcategory
+import Mathlib.CategoryTheory.Products.Basic
+import Mathlib.CategoryTheory.Pi.Basic
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.Combinatorics.Quiver.ConnectedComponent
 
 /-!
 # Groupoids