automated fixes

Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
leanprover-community · Jun 5, 2023 · a9104b0 · a9104b0
1 parent c0efea5
commit a9104b0
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1365,6 +1365,7 @@ import Mathlib.Data.Nat.PrimeNormNum
 import Mathlib.Data.Nat.Set
 import Mathlib.Data.Nat.Size
 import Mathlib.Data.Nat.Sqrt
+import Mathlib.Data.Nat.SqrtNormNum
 import Mathlib.Data.Nat.Squarefree
 import Mathlib.Data.Nat.SuccPred
 import Mathlib.Data.Nat.Totient

diff --git a/Mathlib/Data/Nat/SqrtNormNum.lean b/Mathlib/Data/Nat/SqrtNormNum.lean
@@ -8,8 +8,8 @@ Authors: Mario Carneiro
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Tactic.NormNum
-import Mathbin.Data.Nat.Sqrt
+import Mathlib.Tactic.NormNum
+import Mathlib.Data.Nat.Sqrt
 
 /-! ### `norm_num` plugin for `sqrt`