-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_list_prod [DecidableEq ι] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (l.map fun i ↦ ((l.erase i).map x).prod • proj i).sum x

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
i : Fin l.length
x✝¹ : i ∈ Finset.univ
x✝ : ι → 𝔸'
⊢ (List.map x (List.take (↑i) l)).prod * ((proj l[↑i]) x✝ * (List.map x (List.drop (↑i + 1) l)).prod) =
    (List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod * (proj l[↑i]) x✝

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
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 =
    (List.map (fun i => (List.map x (l.erase i)).prod • proj i) l).sum

Tactic:
conv_rhs => arg 1; arg 2; rw [← List.finRange_map_get l]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
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 =
    (List.map (fun i => (List.map x (l.erase i)).prod • proj i) (List.map l.get (List.finRange l.length))).sum

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
i : Fin l.length
x✝ : i ∈ Finset.univ
⊢ (List.map x (List.take (↑i) l)).prod • (proj l[↑i]).smulRight (List.map x (List.drop (↑i + 1) l)).prod =
    ((List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod) • proj l[↑i]

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
i : Fin l.length
x✝¹ : i ∈ Finset.univ
x✝ : ι → 𝔸'
⊢ ((List.map x (List.take (↑i) l)).prod • (proj l[↑i]).smulRight (List.map x (List.drop (↑i + 1) l)).prod) x✝ =
    (((List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod) • proj l[↑i]) x✝

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
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 =
    (List.map (fun i => (List.map x (l.erase i)).prod • proj i) (List.map l.get (List.finRange l.length))).sum

Tactic:
simp only [List.map_map, ← List.sum_toFinset _ (List.nodup_finRange _), List.toFinset_finRange,
  Function.comp_def, ((List.erase_getElem _).map _).prod_eq, List.eraseIdx_eq_take_drop_succ,
  List.map_append, List.prod_append, List.get_eq_getElem, Fin.getElem_fin, Nat.succ_eq_add_one]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
⊢ ∑ x_1 : Fin l.length,
      (List.map x (List.take (↑x_1) l)).prod • (proj l[↑x_1]).smulRight (List.map x (List.drop (↑x_1 + 1) l)).prod =
    ∑ x_1 : Fin l.length,
      ((List.map x (List.take (↑x_1) l)).prod * (List.map x (List.drop (↑x_1 + 1) l)).prod) • proj l[↑x_1]

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
i : Fin l.length
x✝¹ : i ∈ Finset.univ
x✝ : ι → 𝔸'
⊢ ((List.map x (List.take (↑i) l)).prod • (proj l[↑i]).smulRight (List.map x (List.drop (↑i + 1) l)).prod) x✝ =
    (((List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod) • proj l[↑i]) x✝

Tactic:
simp only [smul_apply, smulRight_apply, smul_eq_mul]

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
i : Fin l.length
x✝¹ : i ∈ Finset.univ
x✝ : ι → 𝔸'
⊢ (List.map x (List.take (↑i) l)).prod * ((proj l[↑i]) x✝ * (List.map x (List.drop (↑i + 1) l)).prod) =
    (List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod * (proj l[↑i]) x✝

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
⊢ ∑ x_1 : Fin l.length,
      (List.map x (List.take (↑x_1) l)).prod • (proj l[↑x_1]).smulRight (List.map x (List.drop (↑x_1 + 1) l)).prod =
    ∑ x_1 : Fin l.length,
      ((List.map x (List.take (↑x_1) l)).prod * (List.map x (List.drop (↑x_1 + 1) l)).prod) • proj l[↑x_1]

Tactic:
exact Finset.sum_congr rfl fun i _ ↦ by
  ext; simp only [smul_apply, smulRight_apply, smul_eq_mul]; ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => (List.map x l).prod) (List.map (fun i => (List.map x (l.erase i)).prod • proj i) l).sum x

Tactic:
refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
l : List ι
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 =
    (List.map (fun i => (List.map x (l.erase i)).prod • proj i) l).sum