R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ ↑derivative (Multiset.prod (Multiset.map f (i ::ₘ s))) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
        (i ::ₘ s))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s : Multiset ι
f : ι → R[X]
⊢ ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
refine' Multiset.induction_on s (by simp) fun i s h => _
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.prod (Multiset.map f s) * ↑derivative (f i) + f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.prod (Multiset.map f s) * ↑derivative (f i) +
      Multiset.sum
        (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
          s)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ ↑derivative (Multiset.prod (Multiset.map f (i ::ₘ s))) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
        (i ::ₘ s))
rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s,
  Multiset.sum_cons, Multiset.erase_cons_head, mul_comm (derivative (f i))]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.prod (Multiset.map f s) * ↑derivative (f i) + f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.prod (Multiset.map f s) * ↑derivative (f i) +
      Multiset.sum
        (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
          s)
congr
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (HMul.hMul (f i))
        (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
  AddMonoidHom.coe_mulLeft]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (fun x => f i * (Multiset.prod (Multiset.map f (Multiset.erase s x)) * ↑derivative (f x))) s) =
    Multiset.sum
      (Multiset.map (fun x => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) x)) * ↑derivative (f x)) s)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (HMul.hMul (f i))
        (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
simp only [Function.comp_apply, Multiset.map_map]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ f i * (Multiset.prod (Multiset.map f (Multiset.erase s j)) * ↑derivative (f j)) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (fun x => f i * (Multiset.prod (Multiset.map f (Multiset.erase s x)) * ↑derivative (f x))) s) =
    Multiset.sum
      (Multiset.map (fun x => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) x)) * ↑derivative (f x)) s)
refine' congr_arg _ (Multiset.map_congr rfl fun j hj => _)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ f i * (Multiset.prod (Multiset.map f (Multiset.erase s j)) * ↑derivative (f j)) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)

case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : ¬i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
by_cases hij : i = j
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s : Multiset ι
f : ι → R[X]
⊢ ↑derivative (Multiset.prod (Multiset.map f 0)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase 0 i)) * ↑derivative (f i)) 0)
simp
no goals
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
simp [hij, ← Multiset.prod_cons, ← Multiset.map_cons, Multiset.cons_erase hj]
no goals
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : ¬i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
simp [hij]