-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup
e_5 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
e_6 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
    UniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
⊢ Eq.{v + 1} (α := F)
    (((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
                (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
                (fa.1.linearDeriv (M₁ := E) fa.2 ∘SL
                  ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))).comp
            (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        g :
      F)
    ((ContinuousLinearMap.comp (M₂ := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
            ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
                fun (x : Option ι) ↦ fa) ∘SL
              ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
                fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
            (ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        g :
      F)
have h : Eq.{v + 1} (α := F) (∑ i : ι, (fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i 0))
  (∑ i : ι,
    (fa.1 : (a : (i : ι) → E i) → F) fun (j : ι) ↦
      (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
            (fun (x : Option ι) ↦ fa) (some i) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
        j)
Tactic: suffices ∑ i, fa.1 (Function.update fa.2 i 0) =
        ∑ i, fa.1 fun j ↦ (Function.update (fun _ ↦ fa) (some i) (g, 0) (some j)).2 j by
      simpa [f, ContinuousLinearMap.continuousMultilinearMapOption]