-- Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
n : ℕ
s : Set E
φ : E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
h₁ :
  ∀ (a : E) (b : (i : Fin n) → E),
    Eq.{u_4 + 1} (α := F)
      (((((restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                      ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                        ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) ∘SL
                    (fderivWithin 𝕜 φ s x :
                      E →L[𝕜] ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
                a :
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
            (a : (i : Fin n) → E) → F)
          b :
        F)
      ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
              (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
                    ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
                (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
              (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
                (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F)
              a :
            (a : (i : Fin n) → E) → F)
          b :
        F)
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F)
    (⇑((restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) ∘SL
          (fderivWithin 𝕜 φ s x : E →L[𝕜] ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)) :
      (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
      (⇑(restrictScalarsLinear (E := fun (x : Fin n) ↦ E) 𝕜 :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (x : Fin n) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin n) ↦ E) F)
      (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x)) :
        (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F))

Tactic:
ext a b