-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
h :
  m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n)
rw :
  HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) *
      m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₁ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) (m • x) : Polynomial ↥(subfield M F))
      (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₂ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₃ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HSMul.hSMul (β := Polynomial ↥(subfield M F)) m Polynomial.X ^ (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
⊢ m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
have rw₄ : HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
  HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
Tactic: rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]