-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
theorem apply_aeval_eq [IsScalarTower R A B] [IsScalarTower A B M'] (d : Derivation R B M')
    (x : B) (p : A[X]) :
    d (aeval x p) = PolynomialModule.eval x ((d.compAlgebraMap A).mapCoeffs p) +
      aeval x (derivative p) • d x

Proof state:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ ∀ (a : A), LinearMap.id ((compAlgebraMap A d) a) = d ((algebraMap A B) a)

Tactic:
intro a

Result:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
a : A
⊢ LinearMap.id ((compAlgebraMap A d) a) = d ((algebraMap A B) a)

Proof state:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ d ((aeval x) p) = (PolynomialModule.eval x) ((compAlgebraMap A d).mapCoeffs p) + (aeval x) (derivative p) • d x

Tactic:
convert apply_aeval_eq' (d.compAlgebraMap A) d LinearMap.id _ x p

Result:
case h.e'_3.h.e'_5.h.e'_6
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ (compAlgebraMap A d).mapCoeffs p = (PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)

R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ ∀ (a : A), LinearMap.id ((compAlgebraMap A d) a) = d ((algebraMap A B) a)

Proof state:
case h.e'_3.h.e'_5.h.e'_6.h
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x✝ : B
p : A[X]
x : ℕ
⊢ ((compAlgebraMap A d).mapCoeffs p) x = ((PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)) x

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ (compAlgebraMap A d).mapCoeffs p = (PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)

Tactic:
apply Finsupp.ext

Result:
case h.e'_3.h.e'_5.h.e'_6.h
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ ∀ (a : ℕ),
    ((compAlgebraMap A d).mapCoeffs p) a = ((PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)) a

Proof state:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
a : A
⊢ LinearMap.id ((compAlgebraMap A d) a) = d ((algebraMap A B) a)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6.h
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ ∀ (a : ℕ),
    ((compAlgebraMap A d).mapCoeffs p) a = ((PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)) a

Tactic:
intro x

Result:
case h.e'_3.h.e'_5.h.e'_6.h
R : Type u_1
A : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
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'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower A B M'
d : Derivation R B M'
x✝ : B
p : A[X]
x : ℕ
⊢ ((compAlgebraMap A d).mapCoeffs p) x = ((PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)) x