awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
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
⊢ 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

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Premises used: Multiset.attach_map_val, Multiset.map_map
-- 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_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
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 :
        𝔸')
⊢ 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))

Tactic:
ext
-- 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_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
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:
simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

Premises used: Finset.sum_multiset_map_count, Multiset.erase_attach_map
-- 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_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) ∘ 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:
exact .congr_fderiv
    (hasStrictFDerivAt_multiset_prod.comp x <|
      hasStrictFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
-- 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_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
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
⊢ 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

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Premises used: Multiset.attach_map_val, Multiset.map_map
-- 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_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
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 :
        𝔸')
⊢ 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))

Tactic:
ext
-- 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_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
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:
simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

Premises used: Finset.sum_multiset_map_count, Multiset.erase_attach_map
-- 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_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) ∘ 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:
exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
-- 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_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
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
⊢ 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

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Premises used: Multiset.attach_map_val, Multiset.map_map
-- 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_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
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 :
        𝔸')
⊢ 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))

Tactic:
ext
-- 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_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
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:
simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

Premises used: Finset.sum_multiset_map_count, Multiset.erase_attach_map
-- 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_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) ∘ 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:
exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
-- 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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, DifferentiableAt.{u_1, u_2, u_7} 𝕜 (F := 𝔸') (fun (x : E) ↦ g i x) x
⊢ Eq (α := E →L[𝕜] 𝔸') (fderiv 𝕜 (fun (x : E) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) u)) x)
    (Multiset.sum
      (Multiset.map
        (fun (i : ι) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (u.erase i)) •> fderiv 𝕜 (g i) x) u))

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

Premises used: HasFDerivAt.multiset_prod, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- 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_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
inst_5 : DecidableEq ι
u : Multiset ι
x : E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ∀ i ∈ u, DifferentiableWithinAt.{u_1, u_2, u_7} 𝕜 (F := 𝔸') (fun (x : E) ↦ g i x) s x
⊢ Eq (α := E →L[𝕜] 𝔸') (fderivWithin 𝕜 (fun (x : E) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) u)) s x)
    (Multiset.sum
      (Multiset.map
        (fun (i : ι) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (u.erase i)) •> fderivWithin 𝕜 (g i) s x)
        u))

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

Premises used: HasFDerivWithinAt.multiset_prod, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- 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_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
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 : 𝔸')
⊢ 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)

Tactic:
ext
-- 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_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
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:
simp [Finset.prod_erase_attach (g · x), ← u.sum_attach]

Premises used: Finset.sum_attach, Finset.prod_erase_attach
-- 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_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
⊢ HasStrictFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸') (fun (x : E) ↦ ∏ i ∈ u, g i x)
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i) x

Tactic:
simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasStrictFDerivAt_finsetProd.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ hg i i.prop)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Premises used: Finset.prod_attach