-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_list_prod' [Fintype ι] {l : List ι} {x : ι → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (∑ i : Fin l.length, ((l.take i).map x).prod •
        smulRight (proj l[i]) ((l.drop (.succ i)).map x).prod) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
⊢ (proj a) x •
        ∑ i : Fin l.length,
          (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod +
      (proj a).smulRight (List.map x l).prod =
    ∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i) (a :: l))).prod •
        (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
x✝ : ι → 𝔸
⊢ ((proj a) x •
          ∑ i : Fin l.length,
            (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod +
        (proj a).smulRight (List.map x l).prod)
      x✝ =
    (∑ i : Fin (a :: l).length,
        (List.map x (List.take (↑i) (a :: l))).prod •
          (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod)
      x✝

Proof state:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
x✝ : ι → 𝔸
⊢ ((proj a) x •
          ∑ i : Fin l.length,
            (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod +
        (proj a).smulRight (List.map x l).prod)
      x✝ =
    (∑ i : Fin (a :: l).length,
        (List.map x (List.take (↑i) (a :: l))).prod •
          (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod)
      x✝

Tactic:
simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm]

Result:
no goals

Proof state:
case cons
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
⊢ HasStrictFDerivAt (fun x => (List.map x (a :: l)).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i) (a :: l))).prod •
        (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod)
    x

Tactic:
simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]

Result:
case cons
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
⊢ HasStrictFDerivAt (fun x => (proj a) x * (List.map x l).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i) (a :: l))).prod •
        (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod)
    x

Proof state:
case nil
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
⊢ HasStrictFDerivAt (fun x => (List.map x []).prod)
    (∑ i : Fin [].length,
      (List.map x (List.take ↑i [])).prod • (proj [][i]).smulRight (List.map x (List.drop (↑i).succ [])).prod)
    x

Tactic:
simp [hasStrictFDerivAt_const]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸
⊢ HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x

Tactic:
induction l with
| nil => simp [hasStrictFDerivAt_const]
| cons a l IH =>
  simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
  exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
    (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

Result:
no goals

Proof state:
case cons
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Fintype ι
x : ι → 𝔸
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x => (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l)).prod • (proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod)
    x
⊢ HasStrictFDerivAt (fun x => (proj a) x * (List.map x l).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i) (a :: l))).prod •
        (proj (a :: l)[i]).smulRight (List.map x (List.drop (↑i).succ (a :: l))).prod)
    x

Tactic:
exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
  (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

Result:
no goals