Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap

Goal state before:
pp: case e'_12.e'_6.hl
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)
this :
  HasStrictFDerivAt (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H))
    ((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2) fg.2
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : instModule ≍ normedSpace.toModule
e_10✝ : instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ : ContinuousMultilinearMap 𝕜 G H
x✝ : (i : ι) → F i
⊢ (((fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)) ∘SL
          ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝ =
    ((((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)).flip
            fg.1 ∘SL
          ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝

pp: case hr
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)
this :
  HasStrictFDerivAt (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H))
    ((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2) fg.2
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : instModule ≍ normedSpace.toModule
e_10✝ : instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ : (i : ι) → F i →L[𝕜] G i
x✝ : (i : ι) → F i
⊢ (((fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)) ∘SL
          ContinuousLinearMap.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝ =
    ((((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)).flip
            fg.1 ∘SL
          ContinuousLinearMap.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝

Tactic:
<;>

Goal state after:
case e'_12.e'_6.hl
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)
this :
  HasStrictFDerivAt (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H))
    ((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2) fg.2
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : instModule ≍ normedSpace.toModule
e_10✝ : instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ : ContinuousMultilinearMap 𝕜 G H
x✝ : (i : ι) → F i
⊢ (((fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)) ∘SL
          ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝ =
    ((((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)).flip
            fg.1 ∘SL
          ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝

case hr
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)
this :
  HasStrictFDerivAt (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H))
    ((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2) fg.2
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : instModule ≍ normedSpace.toModule
e_10✝ : instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ : (i : ι) → F i →L[𝕜] G i
x✝ : (i : ι) → F i
⊢ (((fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)) ∘SL
          ContinuousLinearMap.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝ =
    ((((compContinuousLinearMapContinuousMultilinear 𝕜 F G H).linearDeriv fg.2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)).flip
            fg.1 ∘SL
          ContinuousLinearMap.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
        x✝¹)
      x✝