-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu Fu Gu : Type u}
    [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu]
    [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du}
    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fun y => B (f y) (g y)) s x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Proof state:
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
⊢ ‖iteratedFDerivWithin 𝕜 (n + 1) (fun y => (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1 + 1),
        ↑((n + 1).choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖

Tactic:
have I1 :
    ‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖ := by
  calc
    ‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s x‖ ≤
        ‖B.precompR Du‖ * ∑ i ∈ Finset.range (n + 1),
          n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
            ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
      IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
    _ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
          ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
        mul_le_mul_of_nonneg_right (B.norm_precompR_le Du) (by positivity)
    _ = _ := by
      congr 1
      apply Finset.sum_congr rfl fun i hi => ?_
      rw [Nat.succ_sub (Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)),
        ← norm_iteratedFDerivWithin_fderivWithin hs hx]

Result:
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
I1 :
  ‖iteratedFDerivWithin 𝕜 n (fun y => ((precompR Du B) (f y)) (fderivWithin 𝕜 g s y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖
⊢ ‖iteratedFDerivWithin 𝕜 (n + 1) (fun y => (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1 + 1),
        ↑((n + 1).choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖

Proof state:
case e_a
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
⊢ ∑ i ∈ Finset.range (n + 1),
      ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ =
    ∑ i ∈ Finset.range (n + 1),
      ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖

Tactic:
apply Finset.sum_congr rfl fun i hi => ?_

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ =
    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖