chore(SetTheory/Cardinal/Arithmetic): remove unneeded import (leanprover-community#21013)

Author: vihdzp

Mathlib/Order/Filter/CardinalInter.lean

@@ -6,8 +6,8 @@ Authors: Josha Dekker
 import Mathlib.Order.Filter.Tendsto
 import Mathlib.Order.Filter.Finite
 import Mathlib.Order.Filter.CountableInter
-import Mathlib.SetTheory.Cardinal.Arithmetic
 import Mathlib.SetTheory.Cardinal.Cofinality
+import Mathlib.Tactic.Linarith
 
 /-!
 # Filters with a cardinal intersection property

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Mario Carneiro, Floris van Doorn
 -/
 import Mathlib.SetTheory.Cardinal.Aleph
 import Mathlib.SetTheory.Ordinal.Principal
-import Mathlib.Tactic.Linarith
 
 /-!
 # Cardinal arithmetic
@@ -220,7 +219,7 @@ theorem mul_eq_left_iff {a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧
     rw [← not_lt]
     apply fun h2b => ne_of_gt _ h
     conv_rhs => left; rw [← mul_one n]
-    rw [mul_lt_mul_left]
+    rw [Nat.mul_lt_mul_left]
     · exact id
     apply Nat.lt_of_succ_le h2a
   · rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)