awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x y : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    x
hy :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    y
hxx :
  ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
            (a : Derivation R A' A') → Derivation R A A')
          x.1))
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
            (a : Derivation R A A) → Derivation R A A')
          x.2))
⊢ ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
            (a : Derivation R A' A') → Derivation R A A')
          y.1))
      ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
            (a : Derivation R A A) → Derivation R A A')
          y.2))

Tactic:
have hyy (a : A) := congrArg (fun f => f a) hy
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x y : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    x
hy :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    y
hxx :
  ∀ (a : A),
    Eq (α := A') ((x.1 : (a : A') → A') ((algebraMap A A' : (a : A) → A') a : A') : A')
      ((algebraMap A A' : (a : A) → A') ((x.2 : (a : A) → A) a : A) : A')
hyy :
  ∀ (a : A),
    Eq (α := A') ((y.1 : (a : A') → A') ((algebraMap A A' : (a : A) → A') a : A') : A')
      ((algebraMap A A' : (a : A) → A') ((y.2 : (a : A) → A) a : A) : A')
z : A
⊢ Eq.{u_3 + 1} (α := A')
    (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                (a : Derivation R A' A') → Derivation R A A')
              ⁅x, y⁆.1 :
            Derivation R A A') :
          (a : A) → A')
        z :
      A')
    (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                (a : Derivation R A A) → Derivation R A A')
              ⁅x, y⁆.2 :
            Derivation R A A') :
          (a : A) → A')
        z :
      A')

Tactic:
simp [Derivation.commutator_apply, hxx, hyy]

Premises used: Derivation.commutator_apply
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
mp :
  Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x →
    Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
mpr :
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A)) →
    Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
⊢ Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x ↔
    Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))

Tactic:
constructor
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx : Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
mp :
  ∀ (a : A),
    Eq (α := A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A') a)
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A) a)
⊢ Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx : Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
a : A
⊢ Eq (α := A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A') a)
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A) a)

Tactic:
congrArg (· a) hx

Premises used: congrArg
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx : Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
a : A
⊢ Eq (α := A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A') a)
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A) a)

Tactic:
exact congrArg (· a) hx

Premises used: congrArg
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
mpr :
  ∀ (a : A),
    Eq.{u_3 + 1} (α := A')
      (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                  (a : Derivation R A' A') → Derivation R A A')
                x.1 :
              Derivation R A A') :
            (a : A) → A')
          a :
        A')
      (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                  (a : Derivation R A A) → Derivation R A A')
                x.2 :
              Derivation R A A') :
            (a : A) → A')
          a :
        A')
⊢ Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x

Tactic:
ext a
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
a : A
⊢ Eq.{u_3 + 1} (α := A')
    (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                (a : Derivation R A' A') → Derivation R A A')
              x.1 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')
    (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                (a : Derivation R A A) → Derivation R A A')
              x.2 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')

Tactic:
congrArg (· a) hx

Premises used: congrArg
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
a : A
⊢ Eq.{u_3 + 1} (α := A')
    (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                (a : Derivation R A' A') → Derivation R A A')
              x.1 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')
    (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                (a : Derivation R A A) → Derivation R A A')
              x.2 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')

Tactic:
exact congrArg (· a) hx

Premises used: congrArg
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Derivation R A' A'
y : Derivation R A A
h :
  Eq (α := A → A') (Function.comp (β := A') (⇑x : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑y : (a : A) → A))
⊢ (↑(mk x y h) : Derivation R A' A' × Derivation R A A).1 = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Derivation R A' A'
y : Derivation R A A
h :
  Eq (α := A → A') (Function.comp (β := A') (⇑x : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑y : (a : A) → A))
⊢ (↑(mk x y h) : Derivation R A' A' × Derivation R A A).2 = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : ↥(couple R A A')
a : A
⊢ Eq (α := A')
    (((↑x : Derivation R A' A' × Derivation R A A).1 : (a : A') → A') ((Algebra.ofId A A' : (a : A) → A') a : A') : A')
    ((Algebra.ofId A A' : (a : A) → A') (((↑x : Derivation R A' A' × Derivation R A A).2 : (a : A) → A) a : A) : A')

Tactic:
congrArg (· a) x.2

Premises used: congrArg, Subtype.property
-- Module: Mathlib.RingTheory.Derivation.Lie
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : ↥(couple R A A')
a : A
⊢ Eq (α := A')
    (((↑x : Derivation R A' A' × Derivation R A A).1 : (a : A') → A') ((Algebra.ofId A A' : (a : A) → A') a : A') : A')
    ((Algebra.ofId A A' : (a : A) → A') (((↑x : Derivation R A' A' × Derivation R A A).2 : (a : A) → A) a : A) : A')

Tactic:
exact congrArg (· a) x.2

Premises used: congrArg, Subtype.property
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
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
⊢ Eq (α := ℕ →₀ M) (Finsupp.mapRange (⇑d : (a : A) → M) ⋯ (Finsupp.single 0 1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
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
p q : A[X]
dsimp :
  (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (p * q)) =
    HSMul.hSMul (β := PolynomialModule A M) p
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) p) :
          PolynomialModule A M)
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
          (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
        (a : A[X]) → PolynomialModule A M)
      (p * q) =
    HSMul.hSMul (β := PolynomialModule A M) p
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
                (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
              (a : A[X]) → PolynomialModule A M)
            q :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
                (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
              (a : A[X]) → PolynomialModule A M)
            p :
          PolynomialModule A M)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
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
q p q_1 : A[X]
h :
  (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (p * q)) =
    HSMul.hSMul (β := PolynomialModule A M) p
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) p) :
          PolynomialModule A M)
h_1 :
  (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (q_1 * q)) =
    HSMul.hSMul (β := PolynomialModule A M) q_1
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q_1) :
          PolynomialModule A M)
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) ((p + q_1) * q)) =
    HSMul.hSMul (β := PolynomialModule A M) (p + q_1)
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (p + q_1)) :
          PolynomialModule A M)

Tactic:
simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]

Premises used: add_mul, map_add, add_smul, add_add_add_comm, smul_add
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
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
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
          ((monomial m : (a : A) → A[X]) b : A[X]))) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((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])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)

Tactic:
Finsupp.ext fun i ↦ ?_

Premises used: Finsupp.ext, PolynomialModule
-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
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
monomial :
  ∀ (i : ℕ),
    Eq (α := M)
      ((((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                  (HMul.hMul (α := A[X]) (β := A[X]) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X])
                    ((Polynomial.monomial m : (a : A) → A[X]) b : A[X]))) :
              PolynomialModule A M) :
            (a : ℕ) → M)
          i :
        M)
      ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X])
                ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                    ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                      ((Polynomial.monomial m : (a : A) → A[X]) b)) :
                  PolynomialModule A M) +
              HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((Polynomial.monomial m : (a : A) → A[X]) b : A[X])
                ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                    ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                      ((Polynomial.monomial n : (a : A) → A[X]) a)) :
                  PolynomialModule A M) :
            (a : ℕ) → M)
          i :
        M)
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) (β := A[X]) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X])
          ((Polynomial.monomial m : (a : A) → A[X]) b : A[X]))) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((Polynomial.monomial m : (a : A) → A[X]) b)) :
          PolynomialModule A M) +
      HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((Polynomial.monomial m : (a : A) → A[X]) b : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((Polynomial.monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)

Tactic:
refine Finsupp.ext fun i ↦ ?_

Premises used: Finsupp.ext