Derivative bounds are preserved by a bounded linear rescaling of the value

import Mathlib

open Metric Set Filter Topology BoundedContinuousFunction
open scoped ContDiff

namespace Nemytskii

/-- Let `Ψ : X → E' → F` have `C^∞` partial maps whose derivatives of every order are jointly
continuous and bounded on `X × closedBall 0 R` for every `R`, and let `L : X → E →L[ℝ] E'` be
continuous and bounded. Then `(x, a) ↦ Ψ x (L x a)` has the same properties. -/
theorem iteratedFDeriv_bounds_comp_clm {X : Type*} [TopologicalSpace X]
    {E E' F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F]
    (Ψ : X → E' → F) (hs : ∀ x, ContDiff ℝ ∞ (Ψ x))
    (hc : ∀ k : ℕ, Continuous (fun p : X × E' => iteratedFDeriv ℝ k (Ψ p.1) p.2))
    (hb : ∀ (k : ℕ) (R : ℝ), ∃ C : ℝ, ∀ x, ∀ a ∈ closedBall (0 : E') R,
      ‖iteratedFDeriv ℝ k (Ψ x) a‖ ≤ C)
    (L : X → E →L[ℝ] E') (hL : Continuous L) (Λ : ℝ) (hΛ : ∀ x, ‖L x‖ ≤ Λ) :
    (∀ x, ContDiff ℝ ∞ ((fun x a => Ψ x (L x a)) x)) ∧
      (∀ k : ℕ, Continuous (fun y : X × E => iteratedFDeriv ℝ k ((fun x a => Ψ x (L x a)) y.1) y.2)) ∧
      ∀ (k : ℕ) (R : ℝ), ∃ C : ℝ, ∀ x, ∀ a ∈ closedBall (0 : E) R,
        ‖iteratedFDeriv ℝ k ((fun x a => Ψ x (L x a)) x) a‖ ≤ C := by
  sorry

end Nemytskii