-- 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 :
  ∀ 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)
𝕜₁ :
  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)
𝕜₂ :
  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 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : E) ↦
          (((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
                  (fderivWithin 𝕜 g t (f y)) :
                (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
              (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
            (fderivWithin 𝕜 f s y))
        s x)
𝕜₃ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : E) ↦
          (((ContinuousLinearMap.compL 𝕜 E Fu Gu : (a : Fu →L[𝕜] Gu) → (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu)
                  (fderivWithin 𝕜 g t (f y)) :
                (E →L[𝕜] Fu) →L[𝕜] E →L[𝕜] Gu) :
              (a : E →L[𝕜] Fu) → E →L[𝕜] Gu)
            (fderivWithin 𝕜 f s y))
        s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
            (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
          (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x)
𝕜₄ :
  LE.le (α := ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) (Fu →L[𝕜] Gu))
            (iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ E) (E →L[𝕜] Fu))
          (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x))
    (∑ i ∈ Finset.range (n + 1), (↑(n.choose i) : ℝ) * ((↑i ! : ℝ) * C * D ^ i) * D ^ (n - i + 1))
𝕜₅ :
  Eq (α := ℝ) (∑ i ∈ Finset.range (n + 1), (↑(n.choose i) : ℝ) * ((↑i ! : ℝ) * C * D ^ i) * D ^ (n - i + 1))
    (∑ i ∈ Finset.range (n + 1),
      (↑n ! : ℝ) * HMul.hMul (α := ℝ) (↑i ! : ℝ)⁻¹ (↑i ! : ℝ) * C * (D ^ i * D ^ (n - i + 1)) * (↑(n - i)! : ℝ)⁻¹)
𝕜₆ :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (↑n ! : ℝ) * HMul.hMul (α := ℝ) (↑i ! : ℝ)⁻¹ (↑i ! : ℝ) * C * (D ^ i * D ^ (n - i + 1)) * (↑(n - i)! : ℝ)⁻¹)
    (∑ i ∈ Finset.range (n + 1), HMul.hMul (α := ℝ) (↑n ! : ℝ) 1 * C * D ^ (n + 1) * (↑(n - i)! : ℝ)⁻¹)
𝕜₇ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (n + 1), HMul.hMul (α := ℝ) (↑n ! : ℝ) 1 * C * D ^ (n + 1) * (↑(n - i)! : ℝ)⁻¹)
    (∑ i ∈ Finset.range (n + 1), HMul.hMul (α := ℝ) (↑n ! : ℝ) 1 * C * D ^ (n + 1) * 1)
𝕜₈ :
  ∑ i ∈ Finset.range (n + 1), HMul.hMul (α := ℝ) (↑n ! : ℝ) 1 * C * D ^ (n + 1) * 1 = (↑(n + 1)! : ℝ) * C * D ^ (n + 1)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) ≤
    (↑(n + 1)! : ℝ) * C * D ^ (n + 1)

Tactic:
calc
    ‖iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x‖ =
        ‖iteratedFDerivWithin 𝕜 n (fun y : E => fderivWithin 𝕜 (g ∘ f) s y) s x‖ := by
      rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply,
        LinearIsometryEquiv.norm_map]
    _ = ‖iteratedFDerivWithin 𝕜 n (fun y : E => ContinuousLinearMap.compL 𝕜 E Fu Gu
        (fderivWithin 𝕜 g t (f y)) (fderivWithin 𝕜 f s y)) s x‖ := by
      congr 1
      refine iteratedFDerivWithin_congr (fun y hy => ?_) hx _
      apply fderivWithin_comp _ _ _ hst (hs y hy)
      · exact hg.differentiableOn (by positivity) _ (hst hy)
      · exact hf.differentiableOn (by positivity) _ hy
    -- bound it using the fact that the composition of linear maps is a bilinear operation,
    -- for which we have bounds for the`n`-th derivative.
    _ ≤ ∑ i ∈ Finset.range (n + 1),
        (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ *
          ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ := by
      exact (ContinuousLinearMap.compL 𝕜 E Fu Gu).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
        ((hg.fderivWithin ht (by simp)).comp (hf.of_le M.le) hst) (hf.fderivWithin hs (by simp))
        hs hx le_rfl (ContinuousLinearMap.norm_compL_le 𝕜 E Fu Gu)
    -- bound each of the terms using the estimates on previous derivatives (that use the inductive
    -- assumption for `g' ∘ f`).
    _ ≤ ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * (i ! * C * D ^ i) * D ^ (n - i + 1) := by
      gcongr with i hi
      · exact I i hi
      · exact J i
    -- We are left with trivial algebraic manipulations to see that this is smaller than
    -- the claimed bound.
    _ = ∑ i ∈ Finset.range (n + 1),
        (n ! : ℝ) * ((i ! : ℝ)⁻¹ * i !) * C * (D ^ i * D ^ (n - i + 1)) * ((n - i)! : ℝ)⁻¹ := by
      congr! 1 with i hi
      simp only [Nat.cast_choose ℝ (Finset.mem_range_succ_iff.1 hi), div_eq_inv_mul, mul_inv]
      ring
    _ = ∑ i ∈ Finset.range (n + 1), (n ! : ℝ) * 1 * C * D ^ (n + 1) * ((n - i)! : ℝ)⁻¹ := by
      congr! with i hi
      · exact inv_mul_cancel₀ (by positivity)
      · rw [← pow_add]
        congr 1
        rw [Nat.add_succ, Nat.succ_inj]
        exact Nat.add_sub_of_le (Finset.mem_range_succ_iff.1 hi)
    _ ≤ ∑ i ∈ Finset.range (n + 1), (n ! : ℝ) * 1 * C * D ^ (n + 1) * 1 := by
      gcongr with i
      apply inv_le_one_of_one_le₀
      simpa only [Nat.one_le_cast] using (n - i).factorial_pos
    _ = (n + 1)! * C * D ^ (n + 1) := by
      simp only [mul_assoc, mul_one, Finset.sum_const, Finset.card_range, nsmul_eq_mul,
        Nat.factorial_succ, Nat.cast_mul]

Premises used: Function.comp, ContinuousLinearMap.compL, iteratedFDerivWithin, Nat.cast, Finset.range, fderivWithin, HAdd.hAdd, Nat.factorial, OfNat.ofNat, DFunLike.coe