-- 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:
case h.e_6.h.h.inr
𝕜 : 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
I :
  f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))
i : ι
w : E × ((i : ι) → G i)
j : ι
hij : j ≠ i
⊢ (Function.update (fun x => v) (some i) w (some j)).2 j = Function.update v.2 i (w.2 i) j

Tactic:
simp [hij]

Result:
no goals

Proof state:
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
I :
  f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))
J :
  ∀ (i : ι),
    f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) (some i) =
      ((f v.1).toContinuousLinearMap v.2 i).comp ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))
⊢ (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)))

Tactic:
simp [I, J]

Result:
no goals

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
I :
  f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))
i : ι
w : E × ((i : ι) → G i)
⊢ ((f v.1) fun i_1 => (Function.update (fun x => v) (some i) w (some i_1)).2 i_1) =
    (f v.1) (Function.update v.2 i (w.2 i))

Tactic:
congr

Result:
case h.e_6.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
I :
  f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))
i : ι
w : E × ((i : ι) → G i)
⊢ (fun i_1 => (Function.update (fun x => v) (some i) w (some i_1)).2 i_1) = Function.update v.2 i (w.2 i)

Proof state:
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)))

Tactic:
have I : f.continuousMultilinearMapOption.toContinuousLinearMap (fun _ ↦ v) none =
    (f.flipMultilinear v.2) ∘L (.fst _ _ _) := by
  simp [ContinuousMultilinearMap.toContinuousLinearMap, continuousMultilinearMapOption]
  apply ContinuousLinearMap.ext (fun w ↦ ?_)
  simp

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
I :
  f.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) none =
    (f.flipMultilinear v.2).comp (fst 𝕜 E ((i : ι) → G i))
⊢ (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)))