fix(Algebra/DirectSum/Ring): correct mis-ported lemma names (leanprov…

…er-community#10953)

Co-authored-by: timotree3 <timorcb@gmail.com>

Mathlib/Algebra/DirectSum/Ring.lean

@@ -458,15 +458,15 @@ instance : NatCast (A 0) :=
   ⟨GSemiring.natCast⟩
 
 @[simp]
-theorem ofNatCast (n : ℕ) : of A 0 n = n :=
+theorem of_natCast (n : ℕ) : of A 0 n = n :=
   rfl
-#align direct_sum.of_nat_cast DirectSum.ofNatCast
+#align direct_sum.of_nat_cast DirectSum.of_natCast
 
 /-- The `Semiring` structure derived from `GSemiring A`. -/
 instance GradeZero.semiring : Semiring (A 0) :=
   Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
     (of A 0).map_add (of_zero_mul A) (of A 0).map_nsmul (fun _ _ => of_zero_pow _ _ _)
-    (ofNatCast A)
+    (of_natCast A)
 #align direct_sum.grade_zero.semiring DirectSum.GradeZero.semiring
 
 /-- `of A 0` is a `RingHom`, using the `DirectSum.GradeZero.semiring` structure. -/
@@ -494,7 +494,7 @@ variable [∀ i, AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A]
 instance GradeZero.commSemiring : CommSemiring (A 0) :=
   Function.Injective.commSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
     (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun x n => DFinsupp.single_smul n x)
-    (fun _ _ => of_zero_pow _ _ _) (ofNatCast A)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 #align direct_sum.grade_zero.comm_semiring DirectSum.GradeZero.commSemiring
 
 end CommSemiring
@@ -525,9 +525,9 @@ instance : IntCast (A 0) :=
   ⟨GRing.intCast⟩
 
 @[simp]
-theorem ofIntCast (n : ℤ) : of A 0 n = n := by
+theorem of_intCast (n : ℤ) : of A 0 n = n := by
   rfl
-#align direct_sum.of_int_cast DirectSum.ofIntCast
+#align direct_sum.of_int_cast DirectSum.of_intCast
 
 /-- The `Ring` derived from `GSemiring A`. -/
 instance GradeZero.ring : Ring (A 0) :=
@@ -539,7 +539,7 @@ instance GradeZero.ring : Ring (A 0) :=
     (fun x n =>
       letI : ∀ i, DistribMulAction ℤ (A i) := fun _ => inferInstance
       DFinsupp.single_smul n x)
-    (fun _ _ => of_zero_pow _ _ _) (ofNatCast A) (ofIntCast A)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 #align direct_sum.grade_zero.ring DirectSum.GradeZero.ring
 
 end Ring
@@ -558,7 +558,7 @@ instance GradeZero.commRing : CommRing (A 0) :=
     (fun x n =>
       letI : ∀ i, DistribMulAction ℤ (A i) := fun _ => inferInstance
       DFinsupp.single_smul n x)
-    (fun _ _ => of_zero_pow _ _ _) (ofNatCast A) (ofIntCast A)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 #align direct_sum.grade_zero.comm_ring DirectSum.GradeZero.commRing
 
 end CommRing