-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu Gu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
f : E → Fu
n : ℕ
s : Set E
t : Set Fu
x : E
hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
hz :
  ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
    (hg : ContDiffOn 𝕜 (↑0 : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑0 : ℕ∞ω) f s)
    (hC :
      ∀ i ≤ 0,
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
    (hD :
      ∀ (i : ℕ),
        1 ≤ i →
          i ≤ 0 →
            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 0) ↦ E) Gu)
        (iteratedFDerivWithin 𝕜 0 (g ∘ f) s x) ≤
      (↑0! : ℝ) * C * HPow.hPow (β := ℕ) D 0
hi :
  ∀ (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_7 : NormedAddCommGroup Gu] [inst_8 : 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),
    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)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin n) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 n (g ∘ f) s x) ≤
    (↑n ! : ℝ) * C * D ^ n

Tactic:
induction n using Nat.case_strong_induction_on generalizing Gu with
  | hz =>
    simpa [norm_iteratedFDerivWithin_zero, Nat.factorial_zero, algebraMap.coe_one, one_mul,
      pow_zero, mul_one, comp_apply] using hC 0 le_rfl
  | hi n IH =>
  have M : (n : ℕ∞ω) < n.succ := Nat.cast_lt.2 n.lt_succ_self
  have Cnonneg : 0 ≤ C := (norm_nonneg _).trans (hC 0 bot_le)
  have Dnonneg : 0 ≤ D := by
    have : 1 ≤ n + 1 := by simp only [le_add_iff_nonneg_left, zero_le']
    simpa only [pow_one] using (norm_nonneg _).trans (hD 1 le_rfl this)
  -- use the inductive assumption to bound the derivatives of `g' ∘ f`.
  have I : ∀ i ∈ Finset.range (n + 1),
      ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ i ! * C * D ^ i := by
    intro i hi
    simp only [Finset.mem_range_succ_iff] at hi
    apply IH i hi
    · apply hg.fderivWithin ht
      grw [Nat.cast_succ, hi]
    · apply hf.of_le (Nat.cast_le.2 (hi.trans n.le_succ))
    · intro j hj
      have : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ =
          ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖ := by
        rw [iteratedFDerivWithin_succ_eq_comp_right ht (hst hx), comp_apply,
          LinearIsometryEquiv.norm_map]
      rw [this]
      exact hC (j + 1) (add_le_add (hj.trans hi) le_rfl)
    · intro j hj h'j
      exact hD j hj (h'j.trans (hi.trans n.le_succ))
  -- reformulate `hD` as a bound for the derivatives of `f'`.
  have J : ∀ i, ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1) := by
    intro i
    have : ‖iteratedFDerivWithin 𝕜 (n - i + 1) f s x‖ ≤ D ^ (n - i + 1) :=
      hD (n - i + 1) (by simp) (Nat.succ_le_succ tsub_le_self)
    simpa [iteratedFDerivWithin_succ_eq_comp_right hs hx]
  -- Now put these together: first, notice that we have to bound `D^n (g' ∘ f ⬝ f')`.
  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: Nat.case_strong_induction_on, algebraMap.coe_one, norm_iteratedFDerivWithin_zero, Function.comp, ContinuousLinearMap.compL, iteratedFDerivWithin, Nat.cast, pow_zero, Finset.range, fderivWithin, HAdd.hAdd, Nat.factorial, Function.comp_apply, Nat.factorial_zero, mul_one, OfNat.ofNat, DFunLike.coe, one_mul