∀ (𝕜 : Type u_2) (F : Type u_1) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 F] (x : ℕ × ℕ),
  ∃ s C,
    0 ≤ C ∧
      ∀ (f : SchwartzMap ℝ F) (x_1 : ℝ),
        ‖x_1‖ ^ x.1 * ‖iteratedFDeriv ℝ x.2 (deriv ⇑f) x_1‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 ℝ F)) f