-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f : (a : M) → N)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) :
          M) =
      HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
        ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) x : M) : N)
m : AEval R M a
simp_rw :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
simp_rw₁ :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X)
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
simp_rw₂ :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
            HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) X m) :
        M) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
      HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X
        ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
simp_rw₃ :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
            HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) X m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
      ((f : (a : M) → N) (HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)) : N)
⊢ (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
have simp_rw₄ : (f : (a : M) → N)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
          HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) X m) :
      M) =
  HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
    ((f : (a : M) → N)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) X m) : M) :
      N)
Tactic: simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]