∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  (∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)) →
    (∀ x ∈ Metric.closedBall x₀ ↑a, ContinuousOn (fun x_1 => f x_1 x) (Set.Icc tmin tmax)) →
      (∀ t ∈ Set.Icc tmin tmax, ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f t x‖ ≤ ↑L) →
        ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r → IsPicardLindelof f t₀ x₀ a r L K