-- 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
𝕜 : 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)

Tactic:
ext j

Result:
case h.e_6.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))
i : ι
w : E × ((i : ι) → G i)
j : ι
⊢ (Function.update (fun x => v) (some i) w (some j)).2 j = Function.update v.2 i (w.2 i) j

Proof state:
case h.e_6.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))
i : ι
w : E × ((i : ι) → G i)
j : ι
⊢ (Function.update (fun x => v) (some i) w (some j)).2 j = Function.update v.2 i (w.2 i) j

Tactic:
rcases eq_or_ne j i with rfl | hij

Result:
case h.e_6.h.h.inl
𝕜 : 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))
w : E × ((i : ι) → G i)
j : ι
⊢ (Function.update (fun x => v) (some j) w (some j)).2 j = Function.update v.2 j (w.2 j) j

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

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.continuousMultilinearMapOption.toContinuousLinearMap (fun x => v) (some i)) w =
    (((f v.1).toContinuousLinearMap v.2 i).comp ((proj i).comp (snd 𝕜 E ((i : ι) → G i)))) w

Tactic:
simp only [ContinuousMultilinearMap.toContinuousLinearMap, continuousMultilinearMapOption,
  coe_mk', MultilinearMap.toLinearMap_apply, ContinuousMultilinearMap.coe_coe,
  MultilinearMap.coe_mkContinuous, MultilinearMap.coe_mk, ne_eq, reduceCtorEq,
  not_false_eq_true, Function.update_of_ne, coe_comp', coe_snd', Function.comp_apply,
  proj_apply]

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
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))