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