awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
i : σ
s : σ →₀ ℕ
r : R
⊢ (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) (X i)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((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) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
have monomial : (D : (a : MvPolynomial σ R) → A)
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) (r * 1) : MvPolynomial σ R) (X i)) =
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) (r * 1) : MvPolynomial σ R)
      ((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) (r * 1) : MvPolynomial σ R) : A)
Tactic: 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)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
i : σ
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)
have add : (D : (a : MvPolynomial σ R) → A) (p * X i + 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)
Tactic: rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
i : σ
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)
add :
  (D : (a : MvPolynomial σ R) → A) (p * X i + 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 + 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)
have add₁ : HAdd.hAdd (α := A) (β := A) ((D : (a : MvPolynomial σ R) → A) (p * X i) : A)
    ((D : (a : MvPolynomial σ R) → A) (q * X i) : A) =
  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)
Tactic: rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
i : σ
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)
add :
  (D : (a : MvPolynomial σ R) → A) (p * X i + 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)
add₁ :
  HAdd.hAdd (α := A) (β := A) ((D : (a : MvPolynomial σ R) → A) (p * X i) : A)
      ((D : (a : MvPolynomial σ R) → A) (q * X i) : A) =
    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 + 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)
have add₂ : HAdd.hAdd (α := A) (β := A) ((D : (a : MvPolynomial σ R) → A) (p * X i) : A)
    ((D : (a : MvPolynomial σ R) → A) (q * X i) : A) =
  HSMul.hSMul (β := A) (p + q) ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    HSMul.hSMul (α := MvPolynomial σ R) (X i)
      (HAdd.hAdd (α := A) (β := A) ((D : (a : MvPolynomial σ R) → A) p : A) ((D : (a : MvPolynomial σ R) → A) q : A))
Tactic: rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
have monomial : ∀ (s : σ →₀ ℕ) (r : R),
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) (X i)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((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) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : 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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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)
⊢ (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)
have 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)
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]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (hypothesis)
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 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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 : MvPolynomial σ R
c : R
⊢ (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
have C : (D : (a : MvPolynomial σ R) → A)
    (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
  HSMul.hSMul (β := A) p
      ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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) ((MvPolynomial.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 : MvPolynomial σ R
c : R
C :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (β := MvPolynomial σ R) p ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
have C₁ : (D : (a : MvPolynomial σ R) → A) (c • p) =
  HSMul.hSMul (β := A) p
      ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
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) ((MvPolynomial.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 : MvPolynomial σ R
c : R
C :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
C₁ :
  (D : (a : MvPolynomial σ R) → A) (c • p) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (β := MvPolynomial σ R) p ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
have C₂ : (D : (a : MvPolynomial σ R) → A) (c • p) =
  HSMul.hSMul (β := A) p 0 +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]