σ : Type u_2
R : Type u_1
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
σ : Type u_2
R : Type u_1
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)
refine' ⟨fun H p i => H _ _, fun H => _⟩
σ : Type u_2
R : Type u_1
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
σ : Type u_2
R : Type u_1
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
have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
σ : Type u_2
R : Type u_1
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
σ : Type u_2
R : Type u_1
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
intro p q
no goals
σ : Type u_2
R : Type u_1
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
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)]
σ : Type u_2
R : Type u_1
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
σ : Type u_2
R : Type u_1
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
intro r
no goals
σ : Type u_2
R : Type u_1
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
rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
σ : Type u_2
R : Type u_1
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
σ : Type u_2
R : Type u_1
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
intro p i
case h1
σ : Type u_2
R : Type u_1
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)

case h2
σ : Type u_2
R : Type u_1
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)
σ : Type u_2
R : Type u_1
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
induction' p using MvPolynomial.induction_on' with s r p q hp hq
no goals
case h1
σ : Type u_2
R : Type u_1
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)
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)]
no goals
case h2
σ : Type u_2
R : Type u_1
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)
rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
no goals
case h_C
σ : Type u_2
R : Type u_1
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
rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
case h_add
σ : Type u_2
R : Type u_1
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)
case h_add
σ : Type u_2
R : Type u_1
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
simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]
no goals
case h_add
σ : Type u_2
R : Type u_1
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)
abel
case h_X
σ : Type u_2
R : Type u_1
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)
case h_X
σ : Type u_2
R : Type u_1
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
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
no goals
case h_X
σ : Type u_2
R : Type u_1
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)
rw [smul_comm (X i), smul_comm (X i)]