[Merged by Bors] - chore: drop MulZeroClass. in mul_zero/zero_mul

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -242,7 +242,7 @@ theorem first_vote_pos :
         exact subset_union_left _ _
       rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
         cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
-        count_countedSequence, count_countedSequence, one_mul, MulZeroClass.zero_mul, add_zero,
+        count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
         Nat.cast_add, Nat.cast_one]
       · rw [mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
         · norm_cast

Archive/Wiedijk100Theorems/Partition.lean

@@ -289,7 +289,7 @@ theorem num_series' [Field α] (i : ℕ) :
           rw [Nat.mul_sub_left_distrib, ← hp, ← a_left, mul_one, Nat.add_sub_cancel]
         · rintro ⟨rfl, rfl⟩
           match p with
-          | 0 => rw [MulZeroClass.mul_zero] at hp; cases hp
+          | 0 => rw [mul_zero] at hp; cases hp
           | p + 1 => rw [hp]; simp [mul_add]
       · suffices
           (filter (fun a : ℕ × ℕ => i + 1 ∣ a.fst ∧ a.snd = i + 1) (Nat.antidiagonal n.succ)).card =

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -89,9 +89,9 @@ theorem grading.mul_mem :
       a * b ∈ grading R (i + j)
   | 0, 0, a, b, (ha : a.1 = a.2), (hb : b.1 = b.2) => show a.1 * b.1 = a.2 * b.2 by rw [ha, hb]
   | 0, 1, a, b, (_ : a.1 = a.2), (hb : b.1 = 0) =>
-    show a.1 * b.1 = 0 by rw [hb, MulZeroClass.mul_zero]
-  | 1, 0, a, b, (ha : a.1 = 0), _ => show a.1 * b.1 = 0 by rw [ha, MulZeroClass.zero_mul]
-  | 1, 1, a, b, (ha : a.1 = 0), _ => show a.1 * b.1 = 0 by rw [ha, MulZeroClass.zero_mul]
+    show a.1 * b.1 = 0 by rw [hb, mul_zero]
+  | 1, 0, a, b, (ha : a.1 = 0), _ => show a.1 * b.1 = 0 by rw [ha, zero_mul]
+  | 1, 1, a, b, (ha : a.1 = 0), _ => show a.1 * b.1 = 0 by rw [ha, zero_mul]
 #align counterexample.counterexample_not_prime_but_homogeneous_prime.grading.mul_mem Counterexample.CounterexampleNotPrimeButHomogeneousPrime.grading.mul_mem
 
 end

Counterexamples/Phillips.lean

@@ -313,7 +313,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
   have I2 : ∀ n : ℕ, (n : ℝ) * (ε / 2) ≤ f ↑(s n) := by
     intro n
     induction' n with n IH
-    · simp only [BoundedAdditiveMeasure.empty, id.def, Nat.cast_zero, MulZeroClass.zero_mul,
+    · simp only [BoundedAdditiveMeasure.empty, id.def, Nat.cast_zero, zero_mul,
         Function.iterate_zero, Subtype.coe_mk, Nat.zero_eq]
       rfl
     · have : (↑(s (n + 1)) : Set α) = ↑(s (n + 1)) \ ↑(s n) ∪ ↑(s n) := by

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -502,10 +502,10 @@ def adjoin (s : Set A) : NonUnitalSubalgebra R A :=
         · refine' Submodule.span_induction hb _ _ _ _
           · exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
               (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)
-          · exact fun x _hx => (MulZeroClass.mul_zero x).symm ▸ Submodule.zero_mem _
+          · exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _
           · exact fun x y hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)
           · exact fun r x hx y hy => (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)
-        · exact (MulZeroClass.zero_mul b).symm ▸ Submodule.zero_mem _
+        · exact (zero_mul b).symm ▸ Submodule.zero_mem _
         · exact fun x y => (add_mul x y b).symm ▸ add_mem
         · exact fun r x hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx }
 

Mathlib/Algebra/Algebra/Unitization.lean

@@ -403,7 +403,7 @@ theorem inl_mul [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
     (inl (r₁ * r₂) : Unitization R A) = inl r₁ * inl r₂ :=
   ext rfl <|
     show (0 : A) = r₁ • (0 : A) + r₂ • (0 : A) + 0 * 0 by
-      simp only [smul_zero, add_zero, MulZeroClass.mul_zero]
+      simp only [smul_zero, add_zero, mul_zero]
 #align unitization.inl_mul Unitization.inl_mul
 
 theorem inl_mul_inl [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r₁ r₂ : R) :
@@ -420,24 +420,24 @@ variable (R)
 @[simp]
 theorem inr_mul [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] (a₁ a₂ : A) :
     (↑(a₁ * a₂) : Unitization R A) = a₁ * a₂ :=
-  ext (MulZeroClass.mul_zero _).symm <|
+  ext (mul_zero _).symm <|
     show a₁ * a₂ = (0 : R) • a₂ + (0 : R) • a₁ + a₁ * a₂ by simp only [zero_smul, zero_add]
 #align unitization.coe_mul Unitization.inr_mul
 
 end
 
 theorem inl_mul_inr [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
     (a : A) : ((inl r : Unitization R A) * a) = ↑(r • a) :=
-  ext (MulZeroClass.mul_zero r) <|
+  ext (mul_zero r) <|
     show r • a + (0 : R) • (0 : A) + 0 * a = r • a by
-      rw [smul_zero, add_zero, MulZeroClass.zero_mul, add_zero]
+      rw [smul_zero, add_zero, zero_mul, add_zero]
 #align unitization.inl_mul_coe Unitization.inl_mul_inr
 
 theorem inr_mul_inl [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
     (a : A) : a * (inl r : Unitization R A) = ↑(r • a) :=
-  ext (MulZeroClass.zero_mul r) <|
+  ext (zero_mul r) <|
     show (0 : R) • (0 : A) + r • a + a * 0 = r • a by
-      rw [smul_zero, zero_add, MulZeroClass.mul_zero, add_zero]
+      rw [smul_zero, zero_add, mul_zero, add_zero]
 #align unitization.coe_mul_inl Unitization.inr_mul_inl
 
 instance instMulOneClass [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] :
@@ -446,25 +446,25 @@ instance instMulOneClass [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAct
     one_mul := fun x =>
       ext (one_mul x.1) <|
         show (1 : R) • x.2 + x.1 • (0 : A) + 0 * x.2 = x.2 by
-          rw [one_smul, smul_zero, add_zero, MulZeroClass.zero_mul, add_zero]
+          rw [one_smul, smul_zero, add_zero, zero_mul, add_zero]
     mul_one := fun x =>
       ext (mul_one x.1) <|
         show (x.1 • (0 : A)) + (1 : R) • x.2 + x.2 * (0 : A) = x.2 by
-          rw [smul_zero, zero_add, one_smul, MulZeroClass.mul_zero, add_zero] }
+          rw [smul_zero, zero_add, one_smul, mul_zero, add_zero] }
 #align unitization.mul_one_class Unitization.instMulOneClass
 
 instance instNonAssocSemiring [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] :
     NonAssocSemiring (Unitization R A) :=
   { Unitization.instMulOneClass,
     Unitization.instAddCommMonoid with
     zero_mul := fun x =>
-      ext (MulZeroClass.zero_mul x.1) <|
+      ext (zero_mul x.1) <|
         show (0 : R) • x.2 + x.1 • (0 : A) + 0 * x.2 = 0 by
-          rw [zero_smul, zero_add, smul_zero, MulZeroClass.zero_mul, add_zero]
+          rw [zero_smul, zero_add, smul_zero, zero_mul, add_zero]
     mul_zero := fun x =>
-      ext (MulZeroClass.mul_zero x.1) <|
+      ext (mul_zero x.1) <|
         show x.1 • (0 : A) + (0 : R) • x.2 + x.2 * 0 = 0 by
-          rw [smul_zero, zero_add, zero_smul, MulZeroClass.mul_zero, add_zero]
+          rw [smul_zero, zero_add, zero_smul, mul_zero, add_zero]
     left_distrib := fun x₁ x₂ x₃ =>
       ext (mul_add x₁.1 x₂.1 x₃.1) <|
         show x₁.1 • (x₂.2 + x₃.2) + (x₂.1 + x₃.1) • x₁.2 + x₁.2 * (x₂.2 + x₃.2) =

Mathlib/Algebra/BigOperators/Fin.lean

@@ -353,7 +353,7 @@ theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m
     (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ) := by
   rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
   rintro x hx
-  rw [Pi.single_eq_of_ne hx, Fin.val_zero', MulZeroClass.zero_mul]
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul]
 #align fin_function_fin_equiv_single finFunctionFinEquiv_single
 
 /-- Equivalence between `∀ i : Fin m, Fin (n i)` and `Fin (∏ i : Fin m, n i)`. -/
@@ -437,7 +437,7 @@ theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)]
       j * ∏ j, n (Fin.castLE i.is_lt.le j) := by
   rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
   rintro x hx
-  rw [Pi.single_eq_of_ne hx, Fin.val_zero', MulZeroClass.zero_mul]
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul]
 #align fin_pi_fin_equiv_single finPiFinEquiv_single
 
 namespace List

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -270,7 +270,7 @@ instance categoryFree : Category (Free R C) where
     -- This imitates the proof of associativity for `MonoidAlgebra`.
     simp only [sum_sum_index, sum_single_index, single_zero, single_add, eq_self_iff_true,
       forall_true_iff, forall₃_true_iff, add_mul, mul_add, Category.assoc, mul_assoc,
-      MulZeroClass.zero_mul, MulZeroClass.mul_zero, sum_zero, sum_add]
+      zero_mul, mul_zero, sum_zero, sum_add]
 #align category_theory.category_Free CategoryTheory.categoryFree
 
 namespace Free

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -161,7 +161,7 @@ instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRin
     rw [← f.map_one, ← f.map_zero]
     congr
   replace e : 0 * x = 1 * x := congr_arg (· * x) e
-  rw [one_mul, MulZeroClass.zero_mul, ← f.map_zero] at e
+  rw [one_mul, zero_mul, ← f.map_zero] at e
   exact e
 set_option linter.uppercaseLean3 false in
 #align CommRing.CommRing_has_strict_terminal_objects CommRingCat.commRingCat_hasStrictTerminalObjects

Mathlib/Algebra/CharP/Basic.lean

@@ -177,12 +177,12 @@ theorem CharP.exists [NonAssocSemiring R] : ∃ p, CharP R p :=
                     rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                       Nat.cast_mul,
                       of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
-                      MulZeroClass.zero_mul, add_zero] at H1,
+                      zero_mul, add_zero] at H1,
                     H2⟩)),
           fun H1 => by
           rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
             of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
-            MulZeroClass.zero_mul]⟩⟩⟩
+            zero_mul]⟩⟩⟩
 #align char_p.exists CharP.exists
 
 theorem CharP.exists_unique [NonAssocSemiring R] : ∃! p, CharP R p :=
@@ -582,7 +582,7 @@ instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
       r = 1 * r := by rw [one_mul]
       _ = (1 : ℕ) * r := by rw [Nat.cast_one]
       _ = 0 * r := by rw [CharP.cast_eq_zero]
-      _ = 0 := by rw [MulZeroClass.zero_mul]
+      _ = 0 := by rw [zero_mul]
 
 theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
   false_of_nontrivial_of_subsingleton R
@@ -654,14 +654,14 @@ theorem charP_of_ne_zero (hn : Fintype.card R = n) (hR : ∀ i < n, (i : R) = 0
       intro k
       constructor
       · intro h
-        rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, MulZeroClass.zero_mul,
+        rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, zero_mul,
           add_zero] at h
         rw [Nat.dvd_iff_mod_eq_zero]
         apply hR _ (Nat.mod_lt _ _) h
         rw [← hn, gt_iff_lt, Fintype.card_pos_iff]
         exact ⟨0⟩
       · rintro ⟨k, rfl⟩
-        rw [Nat.cast_mul, H, MulZeroClass.zero_mul] }
+        rw [Nat.cast_mul, H, zero_mul] }
 #align char_p_of_ne_zero charP_of_ne_zero
 
 theorem charP_of_prime_pow_injective (R) [Ring R] [Fintype R] (p : ℕ) [hp : Fact p.Prime] (n : ℕ)

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -35,14 +35,14 @@ theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type*) [CommRing R] (p
     have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
     apply_fun ((↑) : ℕ → R) at hq
     apply_fun (· * ·) a at hq
-    rw [Nat.cast_mul, hch, MulZeroClass.mul_zero, ← mul_assoc, ha, one_mul] at hq
+    rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq
     norm_cast at h₄
     exact h₄ h₃ hq.symm
   · intro h
     rcases(hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
     apply_fun ((↑) : ℤ → R) at hab
     push_cast at hab
-    rw [hch, MulZeroClass.mul_zero, add_zero, mul_comm] at hab
+    rw [hch, mul_zero, add_zero, mul_comm] at hab
     exact isUnit_of_mul_eq_one (p : R) a hab
 #align is_unit_iff_not_dvd_char_of_ring_char_ne_zero isUnit_iff_not_dvd_char_of_ringChar_ne_zero
 
@@ -70,7 +70,7 @@ theorem prime_dvd_char_iff_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : 
   rw [hr, nsmul_eq_mul] at hr₁
   rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
   apply_fun (· * ·) u at hr₁
-  rw [MulZeroClass.mul_zero, ← mul_assoc, hu, one_mul] at hr₁
+  rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁
   exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁
 #align prime_dvd_char_iff_dvd_card prime_dvd_char_iff_dvd_card
 

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -560,7 +560,7 @@ theorem abs_sub_convergents_le' {b : K}
   -- to consider the case `(GeneralizedContinuedFraction.of v).denominators n = 0`.
   rcases (zero_le_of_denom (K := K)).eq_or_gt with
     ((hB : (GeneralizedContinuedFraction.of v).denominators n = 0) | hB)
-  · simp only [hB, MulZeroClass.mul_zero, MulZeroClass.zero_mul, div_zero, le_refl]
+  · simp only [hB, mul_zero, zero_mul, div_zero, le_refl]
   · apply one_div_le_one_div_of_le
     · have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_part_denom nth_part_denom_eq)
       apply_rules [mul_pos]

Mathlib/Algebra/CubicDiscriminant.lean

@@ -135,23 +135,23 @@ theorem toPoly_injective (P Q : Cubic R) : P.toPoly = Q.toPoly ↔ P = Q :=
 #align cubic.to_poly_injective Cubic.toPoly_injective
 
 theorem of_a_eq_zero (ha : P.a = 0) : P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d := by
-  rw [toPoly, ha, C_0, MulZeroClass.zero_mul, zero_add]
+  rw [toPoly, ha, C_0, zero_mul, zero_add]
 #align cubic.of_a_eq_zero Cubic.of_a_eq_zero
 
 theorem of_a_eq_zero' : toPoly ⟨0, b, c, d⟩ = C b * X ^ 2 + C c * X + C d :=
   of_a_eq_zero rfl
 #align cubic.of_a_eq_zero' Cubic.of_a_eq_zero'
 
 theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = C P.c * X + C P.d := by
-  rw [of_a_eq_zero ha, hb, C_0, MulZeroClass.zero_mul, zero_add]
+  rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]
 #align cubic.of_b_eq_zero Cubic.of_b_eq_zero
 
 theorem of_b_eq_zero' : toPoly ⟨0, 0, c, d⟩ = C c * X + C d :=
   of_b_eq_zero rfl rfl
 #align cubic.of_b_eq_zero' Cubic.of_b_eq_zero'
 
 theorem of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly = C P.d := by
-  rw [of_b_eq_zero ha hb, hc, C_0, MulZeroClass.zero_mul, zero_add]
+  rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]
 #align cubic.of_c_eq_zero Cubic.of_c_eq_zero
 
 theorem of_c_eq_zero' : toPoly ⟨0, 0, 0, d⟩ = C d :=

Mathlib/Algebra/DirectLimit.lean

@@ -605,7 +605,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
     -- porting note: RingHom.map_mul was `(restriction _).map_mul`
     rw [RingHom.map_mul, (FreeCommRing.lift _).map_mul, ←
       of.zero_exact_aux2 G f' hyt hj this hjk (Set.subset_union_right (↑s) t), iht,
-      (f' j k hjk).map_zero, MulZeroClass.mul_zero]
+      (f' j k hjk).map_zero, mul_zero]
 #align ring.direct_limit.of.zero_exact_aux Ring.DirectLimit.of.zero_exact_aux
 
 /-- A component that corresponds to zero in the direct limit is already zero in some

Mathlib/Algebra/DirectSum/Internal.lean

@@ -92,8 +92,8 @@ instance gnonUnitalNonAssocSemiring [Add ι] [NonUnitalNonAssocSemiring R] [SetL
     [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMul A] :
     DirectSum.GNonUnitalNonAssocSemiring fun i => A i :=
   { SetLike.gMul A with
-    mul_zero := fun _ => Subtype.ext (MulZeroClass.mul_zero _)
-    zero_mul := fun _ => Subtype.ext (MulZeroClass.zero_mul _)
+    mul_zero := fun _ => Subtype.ext (mul_zero _)
+    zero_mul := fun _ => Subtype.ext (zero_mul _)
     mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun _ _ _ => Subtype.ext (add_mul _ _ _) }
 #align set_like.gnon_unital_non_assoc_semiring SetLike.gnonUnitalNonAssocSemiring
@@ -102,8 +102,8 @@ instance gnonUnitalNonAssocSemiring [Add ι] [NonUnitalNonAssocSemiring R] [SetL
 instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
     [SetLike.GradedMonoid A] : DirectSum.GSemiring fun i => A i :=
   { SetLike.gMonoid A with
-    mul_zero := fun _ => Subtype.ext (MulZeroClass.mul_zero _)
-    zero_mul := fun _ => Subtype.ext (MulZeroClass.zero_mul _)
+    mul_zero := fun _ => Subtype.ext (mul_zero _)
+    zero_mul := fun _ => Subtype.ext (zero_mul _)
     mul_add := fun _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun _ _ _ => Subtype.ext (add_mul _ _ _)
     natCast := fun n => ⟨n, SetLike.nat_cast_mem_graded _ _⟩
@@ -183,12 +183,12 @@ theorem coe_of_mul_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r
     rw [coe_mul_apply_eq_dfinsupp_sum]
     apply (DFinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.zero_mul, ite_self]
+    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
       exact DFinsupp.sum_zero
     simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
     split_ifs with h
     rfl
-    rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, MulZeroClass.mul_zero]
+    rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
 #align direct_sum.coe_of_mul_apply_aux DirectSum.coe_of_mul_apply_aux
 
 theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i, A i) {i : ι}
@@ -198,12 +198,12 @@ theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i,
     rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
     apply (DFinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.mul_zero, ite_self]
+    · simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
       exact DFinsupp.sum_zero
     simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
     split_ifs with h
     rfl
-    rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, MulZeroClass.zero_mul]
+    rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
 #align direct_sum.coe_mul_of_apply_aux DirectSum.coe_mul_of_apply_aux
 
 theorem coe_of_mul_apply_add [AddLeftCancelMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : A i)
@@ -230,7 +230,7 @@ theorem coe_of_mul_apply_of_not_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι)
     rw [coe_mul_apply_eq_dfinsupp_sum]
     apply (DFinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.zero_mul, ite_self]
+    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
       exact DFinsupp.sum_zero
     · rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
       exact fun x _ H => h ((self_le_add_right i x).trans_eq H)
@@ -242,7 +242,7 @@ theorem coe_mul_of_apply_of_not_le (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι)
     rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
     apply (DFinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.mul_zero, ite_self]
+    · simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
       exact DFinsupp.sum_zero
     · rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
       exact fun x _ H => h ((self_le_add_left i x).trans_eq H)

Mathlib/Algebra/DualNumber.lean

@@ -84,7 +84,7 @@ theorem eps_mul_eps [Semiring R] : (ε * ε : R[ε]) = 0 :=
 
 @[simp]
 theorem inr_eq_smul_eps [MulZeroOneClass R] (r : R) : inr r = (r • ε : R[ε]) :=
-  ext (MulZeroClass.mul_zero r).symm (mul_one r).symm
+  ext (mul_zero r).symm (mul_one r).symm
 #align dual_number.inr_eq_smul_eps DualNumber.inr_eq_smul_eps
 
 /-- For two algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`. -/