-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
theorem apply_aeval_eq' (d' : Derivation R B M') (f : M →ₗ[A] M')
    (h : ∀ a, f (d a) = d' (algebraMap A B a)) (x : B) (p : A[X]) :
    d' (aeval x p) = PolynomialModule.eval x (PolynomialModule.map B f (d.mapCoeffs p)) +
      aeval x (derivative p) • d' x

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p : A[X]
⊢ d' ((aeval x) p) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (aeval x) (derivative p) • d' x

Tactic:
induction p using Polynomial.induction_on' with
| h_add => simp_all only [eval_add, map_add, add_smul]; abel
| h_monomial =>
  simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
    PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
    _root_.map_natCast, h]
  rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]

Result:
no goals

Proof state:
case h_add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ d' ((aeval x) (p✝ + q✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs (p✝ + q✝))) +
      (aeval x) (derivative (p✝ + q✝)) • d' x

Tactic:
simp_all only [eval_add, map_add, add_smul]

Result:
case h_add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x +
      ((PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) +
        (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) +
      ((aeval x) (derivative p✝) • d' x + (aeval x) (derivative q✝) • d' x)

Proof state:
case h_add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x +
      ((PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) +
        (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) +
      ((aeval x) (derivative p✝) • d' x + (aeval x) (derivative q✝) • d' x)

Tactic:
abel

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x + x ^ n✝ • d' ((algebraMap A B) a✝) =
    x ^ n✝ • d' ((algebraMap A B) a✝) + ((algebraMap A B) a✝ * ↑n✝ * x ^ (n✝ - 1)) • d' x

Tactic:
rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ d' ((aeval x) ((monomial n✝) a✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs ((monomial n✝) a✝))) +
      (aeval x) (derivative ((monomial n✝) a✝)) • d' x

Tactic:
simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
  PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
  _root_.map_natCast, h]

Result:
case h_monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x + x ^ n✝ • d' ((algebraMap A B) a✝) =
    x ^ n✝ • d' ((algebraMap A B) a✝) + ((algebraMap A B) a✝ * ↑n✝ * x ^ (n✝ - 1)) • d' x