-- 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 : ℕ
s : Set E
h : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ (h : ContDiffWithinAt 𝕜' (↑0 : WithTop ℕ∞) f s x),
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin 0) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin 0) ↦ E)) (iteratedFDerivWithin 𝕜' 0 f s))
      (iteratedFDerivWithin 𝕜 0 f s)
succ :
  ∀ (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),
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin (n + 1)) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin (n + 1)) ↦ E)) (iteratedFDerivWithin 𝕜' (n + 1) f s))
      (iteratedFDerivWithin 𝕜 (n + 1) f s)
⊢ (𝓝[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)

Tactic:
induction n with
  | zero =>
    filter_upwards with a
    ext m
    simp
  | succ n hn =>
    have t₀ := h.of_le (Nat.cast_le.mpr (n.le_add_right 1))
    have t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y := by
      nth_rw 2 [← s.insert_eq_of_mem hx]
      apply h.eventually (by simp)
    filter_upwards [eventually_eventually_nhdsWithin.2 (hn t₀), t₁,
      eventually_mem_nhdsWithin (a := x) (s := s)] with a h₁a h₃a h₄a
    rw [← Filter.EventuallyEq] at h₁a
    ext m
    simp only [Function.comp_apply, coe_restrictScalars, iteratedFDerivWithin_succ_apply_left]
    rw [← (h₁a.fderivWithin' (by tauto)).eq_of_nhdsWithin h₄a,
      fderivWithin_restrictScalars_comp]
    · simp
    · apply h₃a.differentiableWithinAt_iteratedFDerivWithin
      · rw [Nat.cast_lt]
        simp
      · have : UniqueDiffOn 𝕜' s := hs.mono_field
        simpa [s.insert_eq_of_mem h₄a]
    apply hs a h₄a

Premises used: eventually_mem_nhdsWithin, Filter.EventuallyEq, iteratedFDerivWithin_succ_apply_left, ContinuousMultilinearMap.coe_restrictScalars, Function.comp_apply, Nat.cast_lt, fderivWithin_restrictScalars_comp