-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du Eu Fu Gu : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
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
n : ℕ
s : Set Du
x : Du
hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {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 𝕜 (↑0 : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑0 : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 0
          (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 (HAdd.hAdd (α := ℕ) 0 1),
          (↑(Nat.choose 0 i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (0 - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (0 - i) g s x)
succ :
  ∀ (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_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 + 1) : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 (n + 1)
          (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 + 1),
          (↑((n + 1).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)
⊢ 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)

Tactic:
induction n generalizing Eu Fu Gu with
  | zero =>
    simp only [norm_iteratedFDerivWithin_zero, zero_add, Finset.range_one,
      Finset.sum_singleton, Nat.choose_self, Nat.cast_one, one_mul, Nat.sub_zero, ← mul_assoc]
    apply B.le_opNorm₂
  | succ n IH =>
    have In : (n : ℕ∞ω) + 1 ≤ n.succ := by simp only [Nat.cast_succ, le_refl]
    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‖ := by
            gcongr; exact B.norm_precompR_le Du
        _ = _ := 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]
    have I2 :
        ‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x‖ ≤
        ‖B‖ * ∑ i ∈ Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 (i + 1) f s x‖ *
          ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
      calc
        ‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x‖ ≤
            ‖B.precompL Du‖ * ∑ i ∈ Finset.range (n + 1),
              n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
                ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
          IH _ (hf.fderivWithin hs In) (hg.of_le (Nat.cast_le.2 (Nat.le_succ n)))
        _ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1),
            n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
              ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ := by
          gcongr; exact B.norm_precompL_le Du
        _ = _ := by
          congr 1
          apply Finset.sum_congr rfl fun i _ => ?_
          rw [← norm_iteratedFDerivWithin_fderivWithin hs hx]
    have J : iteratedFDerivWithin 𝕜 n
        (fun y : Du => fderivWithin 𝕜 (fun y : Du => B (f y) (g y)) s y) s x =
          iteratedFDerivWithin 𝕜 n (fun y => B.precompR Du (f y)
            (fderivWithin 𝕜 g s y) + B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x := by
      apply iteratedFDerivWithin_congr (fun y hy => ?_) hx
      exact B.fderivWithin_of_bilinear (hf.differentiableOn (by positivity) y hy)
        (hg.differentiableOn (by positivity) y hy) (hs y hy)
    rw [← norm_iteratedFDerivWithin_fderivWithin hs hx, J]
    have A : ContDiffOn 𝕜 n (fun y => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s :=
      (B.precompR Du).isBoundedBilinearMap.contDiff.comp₂_contDiffOn
        (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
    have A' : ContDiffOn 𝕜 n (fun y => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s :=
      (B.precompL Du).isBoundedBilinearMap.contDiff.comp₂_contDiffOn (hf.fderivWithin hs In)
        (hg.of_le (Nat.cast_le.2 (Nat.le_succ n)))
    rw [fun_iteratedFDerivWithin_add_apply (A.contDiffWithinAt hx) (A'.contDiffWithinAt hx) hs hx]
    apply (norm_add_le _ _).trans ((add_le_add I1 I2).trans (le_of_eq ?_))
    simp_rw [← mul_add, mul_assoc]
    congr 1
    exact (Finset.sum_choose_succ_mul
      (fun i j => ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 j g s x‖) n).symm

Premises used: Norm.norm, HMul.hMul, Fin.succ, norm_iteratedFDerivWithin_zero, mul_assoc, Finset.sum_choose_succ_mul, ContinuousLinearMap.zero, iteratedFDerivWithin, zero_add, Finset.sum_singleton, ContinuousLinearMap.le_opNorm₂, Nat.sub_zero, mul_add, Finset.range_one, norm_iteratedFDerivWithin_fderivWithin, Eq.symm, Nat.cast_one, Nat.choose_self, one_mul