-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
y_1 : E
n : ℕ
ihn :
  ∀ {x : E} (h : s =ᶠ[𝓝[{y_1}ᶜ] x] t),
    (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n f s) (iteratedFDerivWithin 𝕜 n f t)
x : E
h : s =ᶠ[𝓝[{y_1}ᶜ] x] t
y : E
hy : ∀ᶠ (x : E) in 𝓝[{y_1}ᶜ] y, s x = t x
succ :
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) s y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
have succ₁ : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
  (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y) :
    ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
  (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y) :
    ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
Tactic: rw [(ihn hy).fderivWithin_eq_of_nhds, fderivWithin_congr_set' _ hy]