no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
t : ↑(Icc v.tMin v.tMax)
⊢ vComp f ↑t = PicardLindelof.toFun v (↑t) (toFun f t)
simp only [vComp, proj_coe]