R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) =
    sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ↑derivative (f * g) = sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
rw [mul_eq_sum_sum, derivative_sum]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) = ?m.362682

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ?m.362682 = sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ R[X]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) =
    sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
trans
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ),
    x ∈ support f →
      ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (x + j)) (coeff f x * a)) b (coeff g b)) =
        (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) x (coeff f x)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (x + j)) (coeff f x * a)) b (coeff g b)) =
    sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
apply Finset.sum_congr rfl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) b (coeff g b)) =
    (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) n (coeff f n)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ),
    x ∈ support f →
      ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (x + j)) (coeff f x * a)) b (coeff g b)) =
        (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) x (coeff f x)
intro n _
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∀ (x : ℕ),
    x ∈ support g →
      ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) x (coeff g x)) =
        (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) x (coeff g x)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) b (coeff g b)) =
    (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) n (coeff f n)
apply Finset.sum_congr rfl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) =
    (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∀ (x : ℕ),
    x ∈ support g →
      ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) x (coeff g x)) =
        (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) x (coeff g x)
intro m _
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) = ?m.363182

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ?m.363182 = (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ (fun x => R[X]) ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) =
    (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)
trans
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = (n + m) • (↑C (coeff f n * coeff g m) * X ^ (n + m - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) =
    (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)
dsimp
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = ↑C (coeff f n * coeff g m * ↑(n + m)) * X ^ (n + m - 1)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = (n + m) • (↑C (coeff f n * coeff g m) * X ^ (n + m - 1))
rw [← smul_mul_assoc, smul_C, nsmul_eq_mul']
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = ↑C (coeff f n * coeff g m * ↑(n + m)) * X ^ (n + m - 1)
exact derivative_C_mul_X_pow _ _
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ), x ∈ support f → ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.362732 x

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ℕ → R[X]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) = ?m.362682
apply Finset.sum_congr rfl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
x : ℕ
a✝ : x ∈ support f
⊢ ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.362732 x

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ℕ → R[X]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ), x ∈ support f → ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.362732 x

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ℕ → R[X]
intro x _
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
x : ℕ
a✝ : x ∈ support f
⊢ ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.362732 x

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ℕ → R[X]
exact derivative_sum
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) = ?m.363182
exact congr_arg _ C_mul_X_pow_eq_monomial.symm
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
hn : n ∈ support f
m : ℕ
hm : m ∈ support g
⊢ (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m) =
    (fun m b => n • (↑C (coeff f n) * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C (coeff f n) * X ^ n * m • (↑C b * X ^ (m - 1)))
      m (coeff g m)
cases n <;> cases m <;>
  simp_rw [add_smul, mul_smul_comm, smul_mul_assoc, X_pow_mul_assoc, ← mul_assoc, ←
    C_mul, mul_assoc, ← pow_add] <;>
  simp [Nat.add_succ, Nat.succ_add, Nat.succ_sub_one, zero_smul, add_comm]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, x • (↑C (coeff f x) * X ^ (x - 1)) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * x_1 • (↑C (coeff g x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    (↑derivative f * sum g fun n a => ↑C a * X ^ n) + (sum f fun n a => ↑C a * X ^ n) * ↑derivative g
simp only [sum, sum_add_distrib, Finset.mul_sum, Finset.sum_mul, derivative_apply]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, x • (↑C (coeff f x) * X ^ (x - 1)) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * x_1 • (↑C (coeff g x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
simp_rw [← smul_mul_assoc, smul_C, nsmul_eq_mul']
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ y in support g, ∑ x in support f, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g y) * X ^ y) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
rw [Finset.sum_comm]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ y in support g, ∑ x in support f, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g y) * X ^ y) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
congr 1
no goals
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
rw [Finset.sum_comm]