-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ i
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (j + 1)) ↦ Fu) Gu)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
        ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 j Fu Gu)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu)) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin j.succ) ↦ Fu) Gu) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin j.succ) ↦ Fu) Gu)
        (iteratedFDerivWithin 𝕜 j (fun (y : Fu) ↦ fderivWithin 𝕜 g t y) t :
          Fu → ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
        (f x))
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (j + 1)) ↦ Fu) Gu)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 j Fu Gu) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu)) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin j.succ) ↦ Fu) Gu)
          (iteratedFDerivWithin 𝕜 j (fun (y : Fu) ↦ fderivWithin 𝕜 g t y) t (f x)) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin j.succ) ↦ Fu) Gu)
rw₂ rw₃ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fun (y : Fu) ↦ fderivWithin 𝕜 g t y) t (f x) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ Fu) (Fu →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (j + 1)) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 (j + 1) g t (f x))

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_right ht (hst hx), comp_apply,
          LinearIsometryEquiv.norm_map]

Premises used: iteratedFDerivWithin_succ_eq_comp_right, LinearIsometryEquiv.norm_map, Function.comp_apply