-- 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
f : E → F
n_1 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ∀ (h : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x),
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
      (iteratedFDerivWithin 𝕜 n f s)
h : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s x
t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x
t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y
a : E
h₁a :
  (𝓝[s] a).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
    (iteratedFDerivWithin 𝕜 n f s)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
m : (i : Fin (n + 1)) → E
h₁ :
  Eq.{u_4 + 1} (α := F)
    ((((fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜' (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
    ((Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
            (restrictScalars 𝕜 (M₁ := fun (x : Fin n) ↦ E))
            (⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a)) :
              (a : E) → ContinuousMultilinearMap 𝕜' (fun (x : Fin n) ↦ E) F)
            (m 0) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
h₂ :
  DifferentiableWithinAt 𝕜' (F := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (x : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜' n f s) s a
h₃ : UniqueDiffWithinAt 𝕜 s a
⊢ Eq.{u_4 + 1} (α := F)
    ((((fderivWithin 𝕜' (iteratedFDerivWithin 𝕜' n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜' (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s a :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)

Tactic:
rw [← (h₁a.fderivWithin' (by tauto)).eq_of_nhdsWithin h₄a,
      fderivWithin_restrictScalars_comp]

Premises used: Filter.EventuallyEq.fderivWithin', Filter.EventuallyEq.eq_of_nhdsWithin, fderivWithin_restrictScalars_comp