chore: HahnSeries.ofPowerSeries_X_pow linter complains on nightly-tes…

…ting (#12529)

On `nightly-testing` `ofPowerSeries_X_pow` becomes a bad simp lemma, because the LHS will simplify. Fix this by adding the missing lemma so the whole proof is just by `simp`, and remove `@[simp]`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -442,6 +442,18 @@ theorem single_mul_single {a b : Γ} {r s : R} :
 
 end NonUnitalNonAssocSemiring
 
+section Semiring
+
+variable [Semiring R]
+
+@[simp]
+theorem single_pow (a : Γ) (n : ℕ) (r : R) : single a r ^ n = single (n • a) (r ^ n) := by
+  induction' n with n IH
+  · simp; rfl
+  · rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
+
+end Semiring
+
 section NonAssocSemiring
 
 variable [NonAssocSemiring R]

Mathlib/RingTheory/HahnSeries/PowerSeries.lean

@@ -142,15 +142,9 @@ theorem ofPowerSeries_X : ofPowerSeries Γ R PowerSeries.X = single 1 1 := by
     simp (config := { contextual := true }) [Ne.symm hn]
 #align hahn_series.of_power_series_X HahnSeries.ofPowerSeries_X
 
-@[simp]
-theorem ofPowerSeries_X_pow {R} [CommSemiring R] (n : ℕ) :
+theorem ofPowerSeries_X_pow {R} [Semiring R] (n : ℕ) :
     ofPowerSeries Γ R (PowerSeries.X ^ n) = single (n : Γ) 1 := by
-  rw [RingHom.map_pow]
-  induction' n with n ih
-  · simp
-    rfl
-  · rw [pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul,
-      Nat.cast_succ, add_comm]
+  simp
 #align hahn_series.of_power_series_X_pow HahnSeries.ofPowerSeries_X_pow
 
 -- Lemmas about converting hahn_series over fintype to and from mv_power_series