{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} →
        {x₀ : E} → {r L : NNReal} → CoeFun (ODE.FunSpace t₀ x₀ r L) fun x => ↑(Set.Icc tmin tmax) → E