-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
      ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
succ :
  Eq.{u_4 + 1} (α := G)
    (((((↑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G) ∘SL
                  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜
                  (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
                    (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) →
                        ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
                    (iteratedFDerivWithin 𝕜 i f s))
                  s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)

Tactic:
rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x hx)]

Premises used: ContinuousLinearEquiv.comp_fderivWithin, ContinuousLinearEquiv.continuousMultilinearMapCongrRight