E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt ((next f).toFun ∘ proj v) (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
⊢ HasDerivWithinAt ((next f).toFun ∘ proj v) (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
haveI : Fact ((t : ℝ) ∈ Icc v.tMin v.tMax) := ⟨t.2⟩
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (fun x => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ)
    (PicardLindelof.toFun v (↑t) (toFun f t)) (Icc v.tMin v.tMax) ↑t
refine' HasDerivWithinAt.const_add _ _
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (vComp f ↑t) (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
rw [vComp_apply_coe] at this
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x =>
    ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
refine' this.congr_of_eventuallyEq_of_mem _ t.coe_prop
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
a✝ : ℝ
ht' : a✝ ∈ Icc v.tMin v.tMax
⊢ (∫ (τ : ℝ) in ↑v.t₀..↑(proj v a✝), vComp f τ) = ∫ (τ : ℝ) in ↑v.t₀..a✝, vComp f τ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
⊢ (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(proj v x), vComp f τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x =>
    ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ
filter_upwards [self_mem_nhdsWithin] with _ ht'
no goals
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)
this :
  HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, vComp f τ) (PicardLindelof.toFun v (↑t) (toFun f t))
    (Icc v.tMin v.tMax) ↑t
a✝ : ℝ
ht' : a✝ ∈ Icc v.tMin v.tMax
⊢ (∫ (τ : ℝ) in ↑v.t₀..↑(proj v a✝), vComp f τ) = ∫ (τ : ℝ) in ↑v.t₀..a✝, vComp f τ
rw [v.proj_of_mem ht']