-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₂ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₃ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HSMul.hSMul (β := P[X]) m X ^ (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₄ :
  map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₅ :
  HMul.hMul (α := Q[X]) (map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)))
      (map (↑g : P →+* Q) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₆ :
  HMul.hMul (α := Q[X]) (β := Q[X]) ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) : Q[X])
      (map (↑g : P →+* Q) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₇ :
  HMul.hMul (α := Q[X]) ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) : Q[X])
      (HPow.hPow (α := Q[X]) (map (↑g : P →+* Q) X) (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₈ :
  HMul.hMul (α := Q[X]) ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) : Q[X])
      (HPow.hPow (α := Q[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₉ : HMul.hMul (α := Q[X]) ((C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) : Q[X]) (HPow.hPow (α := Q[X]) X (n + 1)) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]