-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem hasFDerivAt_uncurry_of_multilinear [DecidableEq ι]
    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) (v : E × Π i, G i) :
    HasFDerivAt (fun (p : E × Π i, G i) ↦ f p.1 p.2)
      ((f.flipMultilinear v.2) ∘L (.fst _ _ _) +
        ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i) ∘L (.proj _) ∘L (.snd _ _ _)) v

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
e_4✝ : Prod.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Prod.instModule = NormedSpace.toModule
e_6✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_8✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
⊢ f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))

Tactic:
simp [ContinuousMultilinearMap.toContinuousLinearMap, continuousMultilinearMapOption]

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
e_4✝ : Prod.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Prod.instModule = NormedSpace.toModule
e_6✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_8✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
⊢ {
      toLinearMap :=
        ({ toFun := fun p => (f (p none).1) fun i => (p (some i)).2 i, map_update_add' := ⋯,
                  map_update_smul' := ⋯ }.mkContinuous
              ‖f‖ ⋯).toLinearMap
          (fun x => v) none,
      cont := ⋯ } =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
e_4✝ : Prod.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Prod.instModule = NormedSpace.toModule
e_6✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_8✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
⊢ {
      toLinearMap :=
        ({ toFun := fun p => (f (p none).1) fun i => (p (some i)).2 i, map_update_add' := ⋯,
                  map_update_smul' := ⋯ }.mkContinuous
              ‖f‖ ⋯).toLinearMap
          (fun x => v) none,
      cont := ⋯ } =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))

Tactic:
apply ContinuousLinearMap.ext (fun w ↦ ?_)

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
e_4✝ : Prod.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Prod.instModule = NormedSpace.toModule
e_6✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_8✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
w : E × ((i : ι) → G i)
⊢ {
        toLinearMap :=
          ({ toFun := fun p => (f (p none).1) fun i => (p (some i)).2 i, map_update_add' := ⋯,
                    map_update_smul' := ⋯ }.mkContinuous
                ‖f‖ ⋯).toLinearMap
            (fun x => v) none,
        cont := ⋯ }
      w =
    ((f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))) w

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
⊢ HasFDerivAt (fun p => (f p.1) p.2)
    ((f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i)) +
      ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i).comp ((proj i).comp (snd 𝕜 E ((i : ι) → G i))))
    v

Tactic:
convert HasFDerivAt.multilinear_comp (f.continuousMultilinearMapOption)
  (g := fun (_ : Option ι) p ↦ p) (g' := fun _ ↦ ContinuousLinearMap.id _ _) (x := v)
  (fun _ ↦ hasFDerivAt_id _)

Result:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → NormedSpace 𝕜 (G i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
e_4✝ : Prod.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Prod.instModule = NormedSpace.toModule
e_6✝ : instTopologicalSpaceProd = UniformSpace.toTopologicalSpace
e_8✝ : NormedAddCommGroup.toAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
⊢ (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i)) +
      ∑ i : ι, ((f v.1).toContinuousLinearMap v.2 i).comp ((proj i).comp (snd 𝕜 E ((i : ι) → G i))) =
    ∑ i : Option ι,
      (f.continuousMultilinearMapOption.toContinuousLinearMap (fun j => v) i).comp (id 𝕜 (E × ((i : ι) → G i)))