case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ (t : ℝ), t ∈ Icc v.tMin v.tMax → HasDerivWithinAt f (toFun v t (f t)) (Icc v.tMin v.tMax) t
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ (t : ℝ), t ∈ Icc v.tMin v.tMax → HasDerivWithinAt f (toFun v t (f t)) (Icc v.tMin v.tMax) t
rcases v.exists_fixed with ⟨f, hf⟩
case intro.refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
⊢ (f.toFun ∘ proj v) ↑v.t₀ = v.x₀

case intro.refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (f.toFun ∘ proj v) (toFun v t ((f.toFun ∘ proj v) t)) (Icc v.tMin v.tMax) t
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ (t : ℝ), t ∈ Icc v.tMin v.tMax → HasDerivWithinAt f (toFun v t (f t)) (Icc v.tMin v.tMax) t
refine' ⟨f ∘ v.proj, _, fun t ht => _⟩
case intro.refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : { x // x ∈ Icc v.tMin v.tMax }
⊢ HasDerivWithinAt (fun x => FunSpace.toFun f (proj v x)) (toFun v (↑t) (FunSpace.toFun f (proj v ↑t)))
    (Icc v.tMin v.tMax) ↑t
case intro.refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (fun x => FunSpace.toFun f (proj v x)) (toFun v t (FunSpace.toFun f (proj v t))) (Icc v.tMin v.tMax)
    t
lift t to Icc v.tMin v.tMax using ht
no goals
case intro.refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : FunSpace v
hf : FunSpace.next f = f
t : { x // x ∈ Icc v.tMin v.tMax }
⊢ HasDerivWithinAt (fun x => FunSpace.toFun f (proj v x)) (toFun v (↑t) (FunSpace.toFun f (proj v ↑t)))
    (Icc v.tMin v.tMax) ↑t
simpa only [hf, v.proj_coe] using f.hasDerivWithinAt_next t