awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst_3 : DecidableEq ι
inst_4 : Finite ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (Multiset.map x u.val).prod)
    (Multiset.sum
      (Multiset.map (fun (x_1 : ι) ↦ (Multiset.map x (u.erase x_1).val).prod •> proj (φ := fun (a : ι) ↦ 𝔸') x_1)
        u.val))
    x

Tactic:
exact hasStrictFDerivAt_multiset_prod

Premises used: hasStrictFDerivAt_multiset_prod
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst_3 : DecidableEq ι
inst_4 : Finite ι
x : ι → 𝔸'
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ ∏ i ∈ u, x i)
    (∑ i ∈ u, (∏ j ∈ u.erase i, x j) •> proj (φ := fun (a : ι) ↦ 𝔸') i) x

Tactic:
have := Fintype.ofFinite ι
  hasStrictFDerivAt_finsetProd.hasFDerivAt

Premises used: Fintype.ofFinite, HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_finsetProd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) ↦ f i x) (f' i) x
simp_rw :
  HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸) (fun (x : E) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) l))
    (∑ i : Fin l.length,
      List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.take (↑i : ℕ) l)) •>
        (f' (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.drop (↑i : ℕ).succ l))))
    x

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

Premises used: List.get_eq_getElem, List.map_map, List.map_get_finRange, Fin.getElem_fin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) ↦ f i x) (f' i) x
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x

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

Premises used: Iff.mpr, List.get, Fin.isLt, List.getElem_mem, HasStrictFDerivAt.comp, HasStrictFDerivAt.congr_fderiv, hasStrictFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) ↦ f i x) (f' i) x
refine :
  Eq (α := E →L[𝕜] 𝔸)
    (comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x

Tactic:
refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
    (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) ↦ f i x) (f' i) x
h₁ :
  ∀ (m : E),
    Eq.{u_6 + 1} (α := 𝔸)
      ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
              (∑ i : Fin l.length,
                List.prod
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
                  (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
                    List.prod
                      (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                        (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
              (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
            (a : E) → 𝔸)
          m :
        𝔸)
      ((∑ x_1 : Fin l.length,
              List.prod
                  (List.map (fun (x_2 : ι) ↦ f x_2 x)
                    (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
                (f' (l.get x_1) <•
                  List.prod
                    (List.map (fun (x_2 : ι) ↦ f x_2 x)
                      (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))) :
            (a : E) → 𝔸)
          m :
        𝔸)
⊢ Eq (α := E →L[𝕜] 𝔸)
    (comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))

Tactic:
ext m
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun (x : E) ↦ f i x) (f' i) x
simp_rw :
  HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸) (fun (x : E) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) l))
    (∑ i : Fin l.length,
      List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.take (↑i : ℕ) l)) •>
        (f' (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.drop (↑i : ℕ).succ l))))
    x

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

Premises used: List.get_eq_getElem, List.map_map, List.map_get_finRange, Fin.getElem_fin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun (x : E) ↦ f i x) (f' i) x
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x

Tactic:
.congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_

Premises used: Iff.mpr, List.get, HasFDerivAt.congr_fderiv, List.get_mem, hasFDerivAt_pi, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun (x : E) ↦ f i x) (f' i) x
refine :
  Eq (α := E →L[𝕜] 𝔸)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    x

Tactic:
refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun (x : E) ↦ f i x) (f' i) x
h₁ :
  ∀ (m : E),
    Eq.{u_6 + 1} (α := 𝔸)
      ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
              (∑ i : Fin l.length,
                List.prod
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
                  (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
                    List.prod
                      (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                        (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
              (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
            (a : E) → 𝔸)
          m :
        𝔸)
      ((∑ x_1 : Fin l.length,
              List.prod
                  (List.map (fun (x_2 : ι) ↦ f x_2 x)
                    (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
                (f' (l.get x_1) <•
                  List.prod
                    (List.map (fun (x_2 : ι) ↦ f x_2 x)
                      (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))) :
            (a : E) → 𝔸)
          m :
        𝔸)
⊢ Eq (α := E →L[𝕜] 𝔸)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))

Tactic:
ext m
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun (x : E) ↦ f i x) (f' i) s x
simp_rw :
  HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸) (fun (x : E) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) l))
    (∑ i : Fin l.length,
      List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.take (↑i : ℕ) l)) •>
        (f' (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.drop (↑i : ℕ).succ l))))
    s x

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

Premises used: List.get_eq_getElem, List.map_map, List.map_get_finRange, Fin.getElem_fin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun (x : E) ↦ f i x) (f' i) s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    s x

Tactic:
.congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_

Premises used: Iff.mpr, List.get, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.congr_fderiv, List.get_mem, hasFDerivWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun (x : E) ↦ f i x) (f' i) s x
refine :
  Eq (α := E →L[𝕜] 𝔸)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : E) ↦ List.prod (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))
    s x

Tactic:
refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun (x : E) ↦ f i x) (f' i) s x
h₁ :
  ∀ (m : E),
    Eq.{u_6 + 1} (α := 𝔸)
      ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
              (∑ i : Fin l.length,
                List.prod
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
                  (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
                    List.prod
                      (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                        (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
              (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
            (a : E) → 𝔸)
          m :
        𝔸)
      ((∑ x_1 : Fin l.length,
              List.prod
                  (List.map (fun (x_2 : ι) ↦ f x_2 x)
                    (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
                (f' (l.get x_1) <•
                  List.prod
                    (List.map (fun (x_2 : ι) ↦ f x_2 x)
                      (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))) :
            (a : E) → 𝔸)
          m :
        𝔸)
⊢ Eq (α := E →L[𝕜] 𝔸)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
      (∑ i : Fin l.length,
        List.prod (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
          (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
            List.prod
              (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
      (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)))
    (∑ x_1 : Fin l.length,
      List.prod (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
        (f' (l.get x_1) <•
          List.prod
            (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))))

Tactic:
ext m
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
l : List ι
x : E
h : ∀ i ∈ l, DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := 𝔸) (fun (x : E) ↦ f i x) x
⊢ Eq (α := E →L[𝕜] 𝔸) (fderiv 𝕜 (fun (x : E) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) l)) x)
    (∑ i : Fin l.length,
      List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.take (↑i : ℕ) l)) •>
        (fderiv 𝕜
            (fun (x : E) ↦ f (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) x)
            x <•
          List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.drop (↑i : ℕ).succ l))))

Tactic:
(HasFDerivAt.list_prod' fun i hi ↦ (h i hi).hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.list_prod'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
l : List ι
x : E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ∀ i ∈ l, DifferentiableWithinAt.{u_1, u_2, u_6} 𝕜 (F := 𝔸) (fun (x : E) ↦ f i x) s x
⊢ Eq (α := E →L[𝕜] 𝔸) (fderivWithin 𝕜 (fun (x : E) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) l)) s x)
    (∑ i : Fin l.length,
      List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.take (↑i : ℕ) l)) •>
        (fderivWithin 𝕜
            (fun (x : E) ↦ f (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) x) s
            x <•
          List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (List.drop (↑i : ℕ).succ l))))

Tactic:
(HasFDerivWithinAt.list_prod' fun i hi ↦ (h i hi).hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.list_prod'