awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 :
      𝔸)
have h₁ : Eq.{u_6 + 1} (α := 𝔸)
  ((ContinuousLinearMap.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
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))
    (∑ 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
have 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
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
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
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_hasFDerivWithinAt x
    (hasFDerivWithinAt_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
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
⊢ 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
-- 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
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
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 :
      𝔸)
have h₁ : Eq.{u_6 + 1} (α := 𝔸)
  ((ContinuousLinearMap.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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun (x : E) ↦ g i x) (g' i) x
⊢ HasStrictFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
    (fun (x : E) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) u))
    (Multiset.sum
      (Multiset.map (fun (i : ι) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (u.erase i)) •> g' i) u))
    x
have simp : HasStrictFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
  (fun (x : E) ↦
    Multiset.prod (Multiset.map ((fun (x_1 : ι) ↦ g x_1 x) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach))
  (Multiset.sum
    (Multiset.map
      ((fun (x_1 : ι) ↦
          Multiset.prod
              (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
            g' x_1) ∘
        Subtype.val (p := fun (x : ι) ↦ x ∈ u))
      u.attach))
  x
Tactic: simp only [← Multiset.attach_map_val u, Multiset.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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun (x : E) ↦ g i x) (g' i) x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (Multiset.sum
        (Multiset.map
          (fun (i : Subtype (Membership.mem u)) ↦
            Multiset.prod (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
              proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
          u.attach))
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (Multiset.sum
      (Multiset.map
        ((fun (x_1 : ι) ↦
            Multiset.prod
                (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                  ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
              g' x_1) ∘
          Subtype.val (p := fun (x : ι) ↦ x ∈ u))
        u.attach))
have h₁ : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (Multiset.sum
              (Multiset.map
                (fun (i : Subtype (Membership.mem u)) ↦
                  Multiset.prod
                      (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
                    proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
                u.attach))
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((Multiset.sum
            (Multiset.map
              ((fun (x_2 : ι) ↦
                  Multiset.prod
                      (Multiset.map (fun (x_3 : ι) ↦ g x_3 x)
                        ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_2)) •>
                    g' x_2) ∘
                Subtype.val (p := fun (x : ι) ↦ x ∈ u))
              u.attach) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
Tactic: ext
-- 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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun (x : E) ↦ g i x) (g' i) x
⊢ HasFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
    (fun (x : E) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) u))
    (Multiset.sum
      (Multiset.map (fun (i : ι) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (u.erase i)) •> g' i) u))
    x
have simp : HasFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
  (fun (x : E) ↦
    Multiset.prod (Multiset.map ((fun (x_1 : ι) ↦ g x_1 x) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach))
  (Multiset.sum
    (Multiset.map
      ((fun (x_1 : ι) ↦
          Multiset.prod
              (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
            g' x_1) ∘
        Subtype.val (p := fun (x : ι) ↦ x ∈ u))
      u.attach))
  x
Tactic: simp only [← Multiset.attach_map_val u, Multiset.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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun (x : E) ↦ g i x) (g' i) x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (Multiset.sum
        (Multiset.map
          (fun (i : Subtype (Membership.mem u)) ↦
            Multiset.prod (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
              proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
          u.attach))
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (Multiset.sum
      (Multiset.map
        ((fun (x_1 : ι) ↦
            Multiset.prod
                (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                  ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
              g' x_1) ∘
          Subtype.val (p := fun (x : ι) ↦ x ∈ u))
        u.attach))
have h₁ : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (Multiset.sum
              (Multiset.map
                (fun (i : Subtype (Membership.mem u)) ↦
                  Multiset.prod
                      (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
                    proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
                u.attach))
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((Multiset.sum
            (Multiset.map
              ((fun (x_2 : ι) ↦
                  Multiset.prod
                      (Multiset.map (fun (x_3 : ι) ↦ g x_3 x)
                        ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_2)) •>
                    g' x_2) ∘
                Subtype.val (p := fun (x : ι) ↦ x ∈ u))
              u.attach) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
Tactic: ext
-- 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
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun (x : E) ↦ g i x) (g' i) s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
    (fun (x : E) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) u))
    (Multiset.sum
      (Multiset.map (fun (i : ι) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (u.erase i)) •> g' i) u))
    s x
have simp : HasFDerivWithinAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸')
  (fun (x : E) ↦
    Multiset.prod (Multiset.map ((fun (x_1 : ι) ↦ g x_1 x) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach))
  (Multiset.sum
    (Multiset.map
      ((fun (x_1 : ι) ↦
          Multiset.prod
              (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
            g' x_1) ∘
        Subtype.val (p := fun (x : ι) ↦ x ∈ u))
      u.attach))
  s x
Tactic: simp only [← Multiset.attach_map_val u, Multiset.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
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun (x : E) ↦ g i x) (g' i) s x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (Multiset.sum
        (Multiset.map
          (fun (i : Subtype (Membership.mem u)) ↦
            Multiset.prod (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
              proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
          u.attach))
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (Multiset.sum
      (Multiset.map
        ((fun (x_1 : ι) ↦
            Multiset.prod
                (Multiset.map (fun (x_2 : ι) ↦ g x_2 x)
                  ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_1)) •>
              g' x_1) ∘
          Subtype.val (p := fun (x : ι) ↦ x ∈ u))
        u.attach))
have h₁ : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (Multiset.sum
              (Multiset.map
                (fun (i : Subtype (Membership.mem u)) ↦
                  Multiset.prod
                      (Multiset.map (fun (i : Subtype (Membership.mem u)) ↦ g (↑i : ι) x) (u.attach.erase i)) •>
                    proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
                u.attach))
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((Multiset.sum
            (Multiset.map
              ((fun (x_2 : ι) ↦
                  Multiset.prod
                      (Multiset.map (fun (x_3 : ι) ↦ g x_3 x)
                        ((Multiset.map (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) u.attach).erase x_2)) •>
                    g' x_2) ∘
                Subtype.val (p := fun (x : ι) ↦ x ∈ u))
              u.attach) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
Tactic: ext
-- 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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (x : ↥u) → 𝔸')
      (∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : ↥u) ↦ 𝔸') i)
      (pi (φ := fun (i : ↥u) ↦ 𝔸') fun (i : ↥u) ↦ g' (↑i : ι)))
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i)
have h : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (x : ↥u) → 𝔸')
            (∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : ↥u) ↦ 𝔸') i)
            (pi (φ := fun (i : ↥u) ↦ 𝔸') fun (i : ↥u) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext
-- 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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (∑ i ∈ u.attach,
        (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i)
have h : ∀ (x_1 : E),
  Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (∑ i ∈ u.attach,
              (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext