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

Tactic:
simp

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

Tactic:
intro i

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

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

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

Tactic:
simp

Result:
no goals