[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
f : σ → A
i : σ
⊢ (1 •
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    f i
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
have : C (σ := σ) a • D f = D (C a * f) := by simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ ↑C a • ↑D f = ↑D (↑C a * f)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : ↑C a • ↑D f = ↑D (↑C a * f)
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
rw [this, C_mul', D.map_smul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
⊢ (∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p) ↔
    ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
[PROOFSTEP]
refine' ⟨fun H p i => H _ _, fun H => _⟩
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
⊢ ∀ (r : R), ↑D (↑C r) = 0
[PROOFSTEP]
intro r
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
r : R
⊢ ↑D (↑C r) = 0
[PROOFSTEP]
rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
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 s r p q hp hq
  ·
    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)]
  · rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
⊢ ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
[PROOFSTEP]
intro p i
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
p : MvPolynomial σ R
i : σ
⊢ ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
[PROOFSTEP]
induction' p using MvPolynomial.induction_on' with s r p q hp hq
[GOAL]
case h1
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
i : σ
s : σ →₀ ℕ
r : R
⊢ ↑D (↑(monomial s) r * X i) = ↑(monomial s) r • ↑D (X i) + X i • ↑D (↑(monomial s) r)
[PROOFSTEP]
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)]
[GOAL]
case h2
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
i : σ
p q : MvPolynomial σ R
hp : ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
hq : ↑D (q * X i) = q • ↑D (X i) + X i • ↑D q
⊢ ↑D ((p + q) * X i) = (p + q) • ↑D (X i) + X i • ↑D (p + q)
[PROOFSTEP]
rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
⊢ ∀ (p q : MvPolynomial σ R), ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
intro p q
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
⊢ ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
induction q using MvPolynomial.induction_on with
| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
⊢ ↑D (p * q) = p • ↑D q + q • ↑D p
[PROOFSTEP]
induction q using MvPolynomial.induction_on with
| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
case h_C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p : MvPolynomial σ R
c : R
⊢ ↑D (p * ↑C c) = p • ↑D (↑C c) + ↑C c • ↑D p
[PROOFSTEP]

| h_C c => rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
[GOAL]
case h_C
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p : MvPolynomial σ R
c : R
⊢ ↑D (p * ↑C c) = p • ↑D (↑C c) + ↑C c • ↑D p
[PROOFSTEP]
rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ ↑D (p * (q₁ + q₂)) = p • ↑D (q₁ + q₂) + (q₁ + q₂) • ↑D p
[PROOFSTEP]

| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ ↑D (p * (q₁ + q₂)) = p • ↑D (q₁ + q₂) + (q₁ + q₂) • ↑D p
[PROOFSTEP]
simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ p • ↑D q₁ + q₁ • ↑D p + (p • ↑D q₂ + q₂ • ↑D p) = p • ↑D q₁ + p • ↑D q₂ + (q₁ • ↑D p + q₂ • ↑D p)
[PROOFSTEP]
abel
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁✝ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q₁ q₂ : MvPolynomial σ R
h₁ : ↑D (p * q₁) = p • ↑D q₁ + q₁ • ↑D p
h₂ : ↑D (p * q₂) = p • ↑D q₂ + q₂ • ↑D p
⊢ p • ↑D q₁ + q₁ • ↑D p + (p • ↑D q₂ + q₂ • ↑D p) = p • ↑D q₁ + p • ↑D q₂ + (q₁ • ↑D p + q₂ • ↑D p)
[PROOFSTEP]
abel
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ ↑D (p * (q * X i)) = p • ↑D (q * X i) + (q * X i) • ↑D p
[PROOFSTEP]

| h_X q i hq =>
  simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
  rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ ↑D (p * (q * X i)) = p • ↑D (q * X i) + (q * X i) • ↑D p
[PROOFSTEP]
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
[GOAL]
case h_X
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : ↑D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), ↑D (↑(monomial s) 1 * X i) = ↑(monomial s) 1 • ↑D (X i) + X i • ↑D (↑(monomial s) 1)
hC : ∀ (r : R), ↑D (↑C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), ↑D (p * X i) = p • ↑D (X i) + X i • ↑D p
p q : MvPolynomial σ R
i : σ
hq : ↑D (p * q) = p • ↑D q + q • ↑D p
⊢ p • q • ↑D (X i) + (X i • p • ↑D q + X i • q • ↑D p) = p • q • ↑D (X i) + (p • X i • ↑D q + q • X i • ↑D p)
[PROOFSTEP]
rw [smul_comm (X i), smul_comm (X i)]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(mkDerivationₗ R f) (↑(monomial s) 1 * X i) =
    ↑(monomial s) 1 • ↑(mkDerivationₗ R f) (X i) + X i • ↑(mkDerivationₗ R f) (↑(monomial s) 1)
[PROOFSTEP]
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum (s + Finsupp.single i 1) fun i_1 k =>
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_add_index'] <;> [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum (s + Finsupp.single i 1) fun i_1 k =>
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_add_index']
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
skip
[GOAL]
case h_zero
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ∀ (a : σ), ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑0 • f a = 0
[PROOFSTEP]
simp
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ∀ (a : σ) (b₁ b₂ : ℕ),
    ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑(b₁ + b₂) • f a =
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₁ • f a +
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a 1)) ↑b₂ • f a
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i a✝ : σ
b₁✝ b₂✝ : ℕ
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑(b₁✝ + b₂✝) • f a✝ =
    ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑b₁✝ • f a✝ +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single a✝ 1)) ↑b₂✝ • f a✝
[PROOFSTEP]
simp only [Nat.cast_add, (monomial _).map_add, add_smul]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
        ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (↑(monomial s) 1 •
        Finsupp.sum (Finsupp.single i 1) fun i_1 k =>
          ↑(monomial (Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    ↑(monomial s) 1 • ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
skip
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑0 • f i = 0
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑0 • f i = 0
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    ↑(monomial s) 1 • ↑(monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i +
      ↑(monomial (Finsupp.single i 1)) 1 • Finsupp.sum s fun i k => ↑(monomial (s - Finsupp.single i 1)) ↑k • f i
[PROOFSTEP]
rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm, Finsupp.smul_sum]
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (↑(monomial s) 1 • f i +
      Finsupp.sum s fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    ↑(monomial s) 1 • f i +
      Finsupp.sum s fun a b => ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single a 1)) ↑b • f a
[PROOFSTEP]
refine' congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => _)
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ (fun i_1 k => ↑(monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) j (↑s j) =
    (fun a b => ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single a 1)) ↑b • f a) j (↑s j)
[PROOFSTEP]
dsimp only
[GOAL]
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ ↑(monomial (s + Finsupp.single i 1 - Finsupp.single j 1)) ↑(↑s j) • f j =
    ↑(monomial (Finsupp.single i 1)) 1 • ↑(monomial (s - Finsupp.single j 1)) ↑(↑s j) • f j
[PROOFSTEP]
rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
[GOAL]
case h
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i j : σ
hj : j ∈ s.support
⊢ Finsupp.single j 1 ≤ s
[PROOFSTEP]
rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
