-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : 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 : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
I1 :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) (Du →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : Du) ↦
          (((precompR Du B : (a : Eu) → (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) (f y) : (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) :
              (a : Du →L[𝕜] Fu) → Du →L[𝕜] Gu)
            (fderivWithin 𝕜 g s y))
        s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)
apply :
  ∀ i ∈ Finset.range (n + 1),
    (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) (Du →L[𝕜] Eu))
            (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (n - i) g s x) =
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (i + 1)) ↦ Du) Eu)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (n - i) g s x)
⊢ Eq (α := ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) (Du →L[𝕜] Eu))
            (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (n - i) g s x))
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (i + 1)) ↦ Du) Eu)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (n - i) g s x))

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

Premises used: Finset.sum_congr, rfl