awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ Eq (α := M)
    ((((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
              (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
                  ((monomial m : (a : A) → A[X]) b : A[X])).toFinsupp :
            PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (toFinsupp ((monomial m : (a : A) → A[X]) b)) :
                PolynomialModule A M) +
            HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (toFinsupp ((monomial n : (a : A) → A[X]) a)) :
                PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
have monomial : Eq (α := M)
  ((((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            (AddMonoidAlgebra.single (n + m) (a * b)) :
          PolynomialModule A M) :
        (a : ℕ) → M)
      i :
    M)
  ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (AddMonoidAlgebra.single m b) :
              PolynomialModule A M) +
          HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (AddMonoidAlgebra.single n a) :
              PolynomialModule A M) :
        (a : ℕ) → M)
      i :
    M)
Tactic: simp only [toFinsupp_mul, toFinsupp_monomial, AddMonoidAlgebra.single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ Eq (α := M)
    ((((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
              (AddMonoidAlgebra.single (n + m) (a * b)) :
            PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (AddMonoidAlgebra.single m b) :
                PolynomialModule A M) +
            HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (AddMonoidAlgebra.single n a) :
                PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
have monomial : (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
  HAdd.hAdd (α := M) (β := M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (AddMonoidAlgebra.single m b) :
              PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (AddMonoidAlgebra.single n a) :
              PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
Tactic: change d _ = _ + _
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
    HAdd.hAdd (α := M) (β := M)
      ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (AddMonoidAlgebra.single m b) :
                PolynomialModule A M) :
            (a : ℕ) → M)
          i :
        M)
      ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
              ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  (AddMonoidAlgebra.single n a) :
                PolynomialModule A M) :
            (a : ℕ) → M)
          i :
        M)
have monomial : (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
  HAdd.hAdd (α := M) (β := M)
    ((HSMul.hSMul (α := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
            (Finsupp.mapRange (⇑d : (a : A) → M) sorry (AddMonoidAlgebra.single m b)) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) ((monomial m : (a : A) → A[X]) b : A[X])
            (Finsupp.mapRange (⇑d : (a : A) → M) sorry (AddMonoidAlgebra.single n a)) :
          (a : ℕ) → M)
        i :
      M)
Tactic: dsimp only [PolynomialModule, Finsupp.mapRange.linearMap_apply, coeFn_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
    HAdd.hAdd (α := M) (β := M)
      ((HSMul.hSMul (α := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
              (Finsupp.mapRange (⇑d : (a : A) → M) ⋯ (AddMonoidAlgebra.single m b)) :
            (a : ℕ) → M)
          i :
        M)
      ((HSMul.hSMul (α := A[X]) ((monomial m : (a : A) → A[X]) b : A[X])
              (Finsupp.mapRange (⇑d : (a : A) → M) ⋯ (AddMonoidAlgebra.single n a)) :
            (a : ℕ) → M)
          i :
        M)
have monomial : (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
  HAdd.hAdd (α := M) (β := M)
    ((HSMul.hSMul (α := A[X]) (β := ℕ →₀ M) ((monomial n : (a : A) → A[X]) a : A[X])
            (Finsupp.single m ((d : (a : A) → M) b) : ℕ →₀ M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := ℕ →₀ M) ((monomial m : (a : A) → A[X]) b : A[X])
            (Finsupp.single n ((d : (a : A) → M) a) : ℕ →₀ M) :
          (a : ℕ) → M)
        i :
      M)
Tactic: rw [Finsupp.mapRange_single, Finsupp.mapRange_single]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
    HAdd.hAdd (α := M) (β := M)
      ((HSMul.hSMul (α := A[X]) (β := ℕ →₀ M) ((monomial n : (a : A) → A[X]) a : A[X])
              (Finsupp.single m ((d : (a : A) → M) b) : ℕ →₀ M) :
            (a : ℕ) → M)
          i :
        M)
      ((HSMul.hSMul (α := A[X]) (β := ℕ →₀ M) ((monomial m : (a : A) → A[X]) b : A[X])
              (Finsupp.single n ((d : (a : A) → M) a) : ℕ →₀ M) :
            (a : ℕ) → M)
          i :
        M)
have monomial : (d : (a : A) → M) ((AddMonoidAlgebra.single (n + m) (a * b) : (a : ℕ) → A) i : A) =
  HAdd.hAdd (α := M) (β := M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
            ((PolynomialModule.single A m : (a : M) → PolynomialModule A M) ((d : (a : A) → M) b) :
              PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
            ((PolynomialModule.single A n : (a : M) → PolynomialModule A M) ((d : (a : A) → M) a) :
              PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
Tactic: change _ = (_ • PolynomialModule.single A _ _) _ + (_ • PolynomialModule.single A _ _) i
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst_6 : CommRing B
inst_7 : Algebra R B
inst_8 : Algebra A B
inst_9 : AddCommGroup M'
inst_10 : Module B M'
inst_11 : Module R M'
inst_12 : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') ((d : (a : A) → M) a : M) : M')
      ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
x : B
n : ℕ
a : A
⊢ (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) ((monomial n : (a : A) → A[X]) a : A[X]) : B) =
    HAdd.hAdd (α := M')
      ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
          (((PolynomialModule.map B f :
                  LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                (a : PolynomialModule A M) → PolynomialModule B M')
              ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) ((monomial n : (a : A) → A[X]) a)) :
            PolynomialModule B M') :
        M')
      (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) ((monomial n : (a : A) → A[X]) a) : A[X]) : B)
        ((d' : (a : B) → M') x : M'))
have monomial : HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) +
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') =
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul (β := M')
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
      ((d' : (a : B) → M') x : M')
Tactic: simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
      PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
      _root_.map_natCast, h]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst_6 : CommRing B
inst_7 : Algebra R B
inst_8 : Algebra A B
inst_9 : AddCommGroup M'
inst_10 : Module B M'
inst_11 : Module R M'
inst_12 : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') ((d : (a : A) → M) a : M) : M')
      ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
x : B
n : ℕ
a : A
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) +
      HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
have monomial : HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul (β := M')
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
      ((d' : (a : B) → M') x : M')
Tactic: rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst_6 : CommRing B
inst_7 : Algebra R B
inst_8 : Algebra A B
inst_9 : AddCommGroup M'
inst_10 : Module B M'
inst_11 : Module R M'
inst_12 : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') ((d : (a : A) → M) a : M) : M')
      ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
x : B
n : ℕ
a : A
monomial :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) +
      HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
have monomial₁ : HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) •
      HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')
Tactic: rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst_6 : CommRing B
inst_7 : Algebra R B
inst_8 : Algebra A B
inst_9 : AddCommGroup M'
inst_10 : Module B M'
inst_11 : Module R M'
inst_12 : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') ((d : (a : A) → M) a : M) : M')
      ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
x : B
n : ℕ
a : A
monomial :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
monomial₁ :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) •
        HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) +
      HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
have monomial₂ : HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (↑n : B) (HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')))
Tactic: rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_4
M' : Type u_5
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : AddCommGroup M'
inst_7 : Module B M'
inst_8 : Module R M'
inst_9 : Module A M'
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ (d : (a : B) → M') ((aeval x : (a : A[X]) → B) p : B) =
    HAdd.hAdd (α := M')
      ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
          ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M') :
        M')
      (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) p : A[X]) : B) ((d : (a : B) → M') x : M'))
have h : Eq.{u_5 + 1} (α := PolynomialModule B M')
  ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M')
  ((PolynomialModule.map B LinearMap.id : (a : PolynomialModule A M') → PolynomialModule B M')
      ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p) :
    PolynomialModule B M')
Tactic: convert! apply_aeval_eq' (d.compAlgebraMap A) d LinearMap.id _ x p
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_4
M' : Type u_5
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : AddCommGroup M'
inst_7 : Module B M'
inst_8 : Module R M'
inst_9 : Module A M'
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
h :
  Eq.{u_5 + 1} (α := PolynomialModule B M')
    ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M')
    ((PolynomialModule.map B LinearMap.id : (a : PolynomialModule A M') → PolynomialModule B M')
        ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p) :
      PolynomialModule B M')
⊢ (d : (a : B) → M') ((aeval x : (a : A[X]) → B) p : B) =
    HAdd.hAdd (α := M')
      ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
          ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M') :
        M')
      (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) p : A[X]) : B) ((d : (a : B) → M') x : M'))
have convert! : ∀ (a : A),
  Eq.{u_5 + 1} (α := M') ((LinearMap.id : (a : M') → M') ((compAlgebraMap A d : (a : A) → M') a : M') : M')
    ((d : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
Tactic: convert! apply_aeval_eq' (d.compAlgebraMap A) d LinearMap.id _ x p
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_4
M' : Type u_5
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : AddCommGroup M'
inst_7 : Module B M'
inst_8 : Module R M'
inst_9 : Module A M'
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower A B M'
d : Derivation R B M'
x : B
p : A[X]
⊢ Eq.{u_5 + 1} (α := PolynomialModule B M')
    ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M')
    ((PolynomialModule.map B LinearMap.id : (a : PolynomialModule A M') → PolynomialModule B M')
        ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p) :
      PolynomialModule B M')
have h : ∀ (a : ℕ),
  Eq.{u_5 + 1} (α := M')
    ((((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p : PolynomialModule A M') : (a : ℕ) → M')
        a :
      M')
    ((((PolynomialModule.map B LinearMap.id : (a : PolynomialModule A M') → PolynomialModule B M')
              ((mapCoeffs (compAlgebraMap A d) : (a : A[X]) → PolynomialModule A M') p) :
            PolynomialModule B M') :
          (a : ℕ) → M')
        a :
      M')
Tactic: apply Finsupp.ext
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
inst_2 : CommRing R
inst_3 : Differential R
inst_4 : Algebra A R
inst_5 : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ((aeval x : (a : A[X]) → R) p : R)′ =
    HAdd.hAdd (α := R) ((aeval x : (a : A[X]) → R) ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) : R)
      (HMul.hMul (α := R) (β := R) ((aeval x : (a : A[X]) → R) ((derivative : (a : A[X]) → A[X]) p : A[X]) : R)
        (x′ : R))
have h : Eq.{u_2 + 1} (α := R) ((aeval x : (a : A[X]) → R) ((mapCoeffs : (a : A[X]) → A[X]) p : A[X]) : R)
  ((PolynomialModule.eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.map R (Algebra.linearMap A R) : (a : PolynomialModule A A) → PolynomialModule R R)
          ((Derivation.mapCoeffs deriv : (a : A[X]) → PolynomialModule A A) p) :
        PolynomialModule R R) :
    R)
Tactic: convert! Derivation.apply_aeval_eq' Differential.deriv _ (Algebra.linearMap A R) ..