awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x
have have : ∀ (this : Fintype ι),
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x
have refine : Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
  (∑ i : Fin l.length,
    (List.map x (List.take (↑i : ℕ) l)).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸')
          (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i sorry) <•
        (List.map x (List.drop (↑i : ℕ).succ l)).prod))
  (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l))
Tactic: refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)
have arg : List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l
have arg : l
Tactic: arg 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| l
have rw : List.map l.get (List.finRange l.length)
Tactic: rw [← List.map_get_finRange l]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)
have arg : List.map l.get (List.finRange l.length)
Tactic: arg 1; arg 2; rw [← List.map_get_finRange l]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l))
have conv_rhs : Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
  (∑ i : Fin l.length,
    (List.map x (List.take (↑i : ℕ) l)).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸')
          (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i sorry) <•
        (List.map x (List.drop (↑i : ℕ).succ l)).prod))
  (List.sum
    (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i)
      (List.map l.get (List.finRange l.length))))
Tactic: conv_rhs => arg 1; arg 2; rw [← List.map_get_finRange l]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum
      (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i)
        (List.map l.get (List.finRange l.length))))
have simp : Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
  (∑ x_1 : Fin l.length,
    (List.map x (List.take (↑x_1 : ℕ) l)).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) sorry) <•
        (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 (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) sorry))
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
h : Membership.mem (γ := Finset (Fin l.length)) Finset.univ i
⊢ (List.map x (List.take (↑i : ℕ) l)).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) <•
        (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 (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)
have h : ∀ (x_1 : ι → 𝔸'),
  Eq.{u_7 + 1} (α := 𝔸')
    (((List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) <•
              (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
    ((((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) •>
            proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
h : Membership.mem (γ := Finset (Fin l.length)) Finset.univ i
x_1 : ι → 𝔸'
⊢ Eq.{u_7 + 1} (α := 𝔸')
    (((List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) <•
              (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
    ((((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) •>
            proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
have h : (List.map x (List.take (↑i : ℕ) l)).prod *
    HMul.hMul (β := 𝔸') (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod
      ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) :
            (a : ι → 𝔸') → 𝔸')
          x_1 :
        𝔸') =
  HMul.hMul (β := 𝔸') ((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod)
    ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) sorry) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
Tactic: simp only [smul_apply, op_smul_eq_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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 : ι → 𝔸') ↦ ∏ i ∈ u, x i)
    (∑ i ∈ u, (∏ j ∈ u.erase i, x j) •> proj (φ := fun (a : ι) ↦ 𝔸') i) x
have simp : 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: simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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))
    (∑ 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
have 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
Tactic: simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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
have 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))))))
Tactic: refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
    (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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
⊢ 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))))))
have 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 :
      𝔸)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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
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 :
      𝔸)
have h₁ : Eq.{u_6 + 1} (α := 𝔸)
  ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
          (∑ x_1 : Fin l.length,
            List.prod
                (List.take (↑x_1 : ℕ) (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length))) •>
              (proj (φ := fun (a : Fin l.length) ↦ 𝔸) x_1 <•
                List.prod
                  (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                    (List.drop (↑x_1 : ℕ).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.take (↑x_1 : ℕ) (List.map (fun (x_2 : ι) ↦ f x_2 x) (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 :
    𝔸)
Tactic: simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    proj_apply, pi_apply, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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))
    (∑ 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
have 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
Tactic: simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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
have 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))))))
Tactic: refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
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
⊢ 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))))))
have 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 :
      𝔸)
Tactic: ext m