awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)

Tactic:
have : C (σ := σ) a • D f = D (C a * f) := by simp
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this :
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)
rw :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
rw₁ : (D : (a : MvPolynomial σ R) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
rw₂ rw₃ :
  HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)

Tactic:
rw [this, C_mul', D.map_smul]

Premises used: MvPolynomial.C_mul', Derivation.map_smul
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D₁ D₂ : Derivation R (MvPolynomial σ R) A
s : Set σ
h :
  Set.EqOn.{u_1, u_3} (β := A) (Function.comp (β := MvPolynomial σ R) (⇑D₁ : (a : MvPolynomial σ R) → A) X)
    (Function.comp (β := MvPolynomial σ R) (⇑D₂ : (a : MvPolynomial σ R) → A) X) s
f : MvPolynomial σ R
hf : Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) f
⊢ Eq.{u_3 + 1} (α := A) ((D₁ : (a : MvPolynomial σ R) → A) f : A) ((D₂ : (a : MvPolynomial σ R) → A) f : A)

Tactic:
Derivation.eqOn_adjoin (Set.forall_mem_image.2 h) hf

Premises used: Iff.mpr, Derivation.eqOn_adjoin, Set.forall_mem_image
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D₁ D₂ : Derivation R (MvPolynomial σ R) A
f : MvPolynomial σ R
h :
  ∀ i ∈ f.vars,
    Eq.{u_3 + 1} (α := A) ((D₁ : (a : MvPolynomial σ R) → A) (X i) : A) ((D₂ : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ Eq.{u_3 + 1} (α := A) ((D₁ : (a : MvPolynomial σ R) → A) f : A) ((D₂ : (a : MvPolynomial σ R) → A) f : A)

Tactic:
derivation_eqOn_supported h f.mem_supported_vars

Premises used: MvPolynomial.mem_supported_vars, MvPolynomial.derivation_eqOn_supported
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
f : MvPolynomial σ R
h : ∀ i ∈ f.vars, Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (X i) : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) f : A) (0 : A)

Tactic:
show D f = (0 : Derivation R (MvPolynomial σ R) A) f from derivation_eq_of_forall_mem_vars h

Premises used: MvPolynomial.derivation_eq_of_forall_mem_vars
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D₁ D₂ : Derivation R (MvPolynomial σ R) A
h :
  ∀ (i : σ),
    Eq.{u_3 + 1} (α := A) ((D₁ : (a : MvPolynomial σ R) → A) (X i) : A) ((D₂ : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ D₁ = D₂

Tactic:
Derivation.ext fun _ => derivation_eq_of_forall_mem_vars fun i _ => h i

Premises used: MvPolynomial.derivation_eq_of_forall_mem_vars, Derivation.ext
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
⊢ (∀ (p q : MvPolynomial σ R),
      (D : (a : MvPolynomial σ R) → A) (p * q) =
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
          HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)) ↔
    ∀ (s : σ →₀ ℕ) (i : σ),
      (D : (a : MvPolynomial σ R) → A)
          (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
            ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
            ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)

Tactic:
⟨fun H p i => H _ _, fun H => ?_⟩

Premises used: MvPolynomial.monomial, MvPolynomial.X, Iff.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
refine :
  ∀
    (H :
      ∀ (s : σ →₀ ℕ) (i : σ),
        (D : (a : MvPolynomial σ R) → A)
            (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
              ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
            HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
              ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A))
    (p q : MvPolynomial σ R),
    (D : (a : MvPolynomial σ R) → A) (p * q) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
        HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (∀ (p q : MvPolynomial σ R),
      (D : (a : MvPolynomial σ R) → A) (p * q) =
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
          HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)) ↔
    ∀ (s : σ →₀ ℕ) (i : σ),
      (D : (a : MvPolynomial σ R) → A)
          (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
            ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
            ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)

Tactic:
refine ⟨fun H p i => H _ _, fun H => ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
r : R
rw : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (HSMul.hSMul (β := MvPolynomial σ R) r 1) : A) (0 : A)
rw₁ : HSMul.hSMul (β := A) r ((D : (a : MvPolynomial σ R) → A) 1 : A) = 0
rw₂ : HSMul.hSMul (β := A) r 0 = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := A) 0 0
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)

Tactic:
rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]

Premises used: smul_zero, LinearMap.map_smul, MvPolynomial.C_eq_smul_one
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
⊢ ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)

Tactic:
have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
p : MvPolynomial σ R
i : σ
monomial :
  ∀ (s : σ →₀ ℕ) (r : R),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A)
          ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A)
              ((MvPolynomial.monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) :
            A)
add :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      (D : (a : MvPolynomial σ R) → A) (p * X i) =
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
    (hq :
      (D : (a : MvPolynomial σ R) → A) (q * X i) =
        HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A)),
    (D : (a : MvPolynomial σ R) → A) ((p + q) * X i) =
      HSMul.hSMul (β := A) (p + q) ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) (p + q) : A)
⊢ (D : (a : MvPolynomial σ R) → A) (p * X i) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)

Tactic:
induction p using MvPolynomial.induction_on' with
    | monomial s r =>
      rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc,
        smul_add, D.map_smul, smul_comm r (X i)]
    | add p q hp hq => rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]

Premises used: add_mul, smul_assoc, mul_assoc, MvPolynomial.monomial, MvPolynomial.C_mul_monomial, map_add, MvPolynomial.C_mul', add_smul, LinearMap.map_smul, add_add_add_comm, smul_add
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
⊢ ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)

Tactic:
have : ∀ p i, D (p * X i) = p • D (X i) + (X i : MvPolynomial σ R) • D p := by
    intro p i
    induction p using MvPolynomial.induction_on' with
    | monomial s r =>
      rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc,
        smul_add, D.map_smul, smul_comm r (X i)]
    | add p q hp hq => rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁_1 : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q₁ q₂ : MvPolynomial σ R
h₁ :
  (D : (a : MvPolynomial σ R) → A) (p * q₁) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
      HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A)
h₂ :
  (D : (a : MvPolynomial σ R) → A) (p * q₂) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)
add :
  HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
        HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
      (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
        HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      (HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
        HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A))
⊢ (D : (a : MvPolynomial σ R) → A) (p * (q₁ + q₂)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (q₁ + q₂) : A) +
      HSMul.hSMul (β := A) (q₁ + q₂) ((D : (a : MvPolynomial σ R) → A) p : A)

Tactic:
simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]

Premises used: map_add, add_smul, mul_add, smul_add
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁_1 : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q₁ q₂ : MvPolynomial σ R
h₁ :
  (D : (a : MvPolynomial σ R) → A) (p * q₁) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
      HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A)
h₂ :
  (D : (a : MvPolynomial σ R) → A) (p * q₂) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
        HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
      (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
        HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      (HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
        HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A))

Tactic:
abel
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
i : σ
hq :
  (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
mul_X :
  p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A)) +
        HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
    p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
        q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
⊢ (D : (a : MvPolynomial σ R) → A) (p * (q * X i)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (q * X i) : A) +
      HSMul.hSMul (β := A) (q * X i) ((D : (a : MvPolynomial σ R) → A) p : A)

Tactic:
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]

Premises used: add_assoc, mul_assoc, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
simp :
  ((s + Finsupp.single i 1).sum fun (i_1 : σ) (k : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) :
                (a : R) → MvPolynomial σ R)
              (↑k : R))
            (f i_1)) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
        (s.sum fun (i : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i))
⊢ (mkDerivationₗ R f : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        ((mkDerivationₗ R f : (a : MvPolynomial σ R) → A) (X i) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
        ((mkDerivationₗ R f : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)

Tactic:
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]

Premises used: MvPolynomial.X, MvPolynomial.mkDerivationₗ_monomial, one_smul, MvPolynomial.monomial_mul, one_mul