-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.list_prod' {l : List ι} {x : E}
    (h : ∀ i ∈ l, HasStrictFDerivAt (f i ·) (f' i) x) :
    HasStrictFDerivAt (fun x ↦ (l.map (f · x)).prod)
      (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
        smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
⊢ (∑ i : Fin l.length,
          (List.map (fun i => f (l.get i) x) (List.take (↑i) (List.finRange l.length))).prod •
            (proj i).smulRight
              (List.map (fun i => f (l.get i) x) (List.drop (↑i).succ (List.finRange l.length))).prod).comp
      (pi fun i => f' (l.get i)) =
    ∑ x_1 : Fin l.length,
      (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
        (f' (l.get x_1)).smulRight
          (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod

Tactic:
ext m

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
m : E
⊢ ((∑ i : Fin l.length,
            (List.map (fun i => f (l.get i) x) (List.take (↑i) (List.finRange l.length))).prod •
              (proj i).smulRight
                (List.map (fun i => f (l.get i) x) (List.drop (↑i).succ (List.finRange l.length))).prod).comp
        (pi fun i => f' (l.get i)))
      m =
    (∑ x_1 : Fin l.length,
        (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
          (f' (l.get x_1)).smulRight
            (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod)
      m

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
m : E
⊢ ((∑ i : Fin l.length,
            (List.map (fun i => f (l.get i) x) (List.take (↑i) (List.finRange l.length))).prod •
              (proj i).smulRight
                (List.map (fun i => f (l.get i) x) (List.drop (↑i).succ (List.finRange l.length))).prod).comp
        (pi fun i => f' (l.get i)))
      m =
    (∑ x_1 : Fin l.length,
        (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
          (f' (l.get x_1)).smulRight
            (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod)
      m

Tactic:
simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
  smulRight_apply, proj_apply, pi_apply, Function.comp_def]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x => (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.finRange l.length)).prod)
    (∑ x_1 : Fin l.length,
      (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
        (f' (l.get x_1)).smulRight
          (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod)
    x

Tactic:
refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
  (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
⊢ (∑ i : Fin l.length,
          (List.map (fun i => f (l.get i) x) (List.take (↑i) (List.finRange l.length))).prod •
            (proj i).smulRight
              (List.map (fun i => f (l.get i) x) (List.drop (↑i).succ (List.finRange l.length))).prod).comp
      (pi fun i => f' (l.get i)) =
    ∑ x_1 : Fin l.length,
      (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
        (f' (l.get x_1)).smulRight
          (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod)
    (∑ i : Fin l.length,
      (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
        (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod)
    x

Tactic:
simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x => (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.finRange l.length)).prod)
    (∑ x_1 : Fin l.length,
      (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •
        (f' (l.get x_1)).smulRight
          (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod)
    x