-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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 :
  ∀ i ∈ Finset.range (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
        (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) ≤
      (↑i ! : ℝ) * C * D ^ i
J :
  ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
        (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x) ≤
      D ^ (n - i + 1)
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
        ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E Gu)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu)) →
              ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin n.succ) ↦ E) Gu) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu)) →
            ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin n.succ) ↦ E) Gu)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
        x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
rw₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E Gu) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu)) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x) :
        ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin n.succ) ↦ E) Gu) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) =
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
have rw₂ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
    (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu)) =
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
    (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply,
        LinearIsometryEquiv.norm_map]