-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem hasDerivWithinAt_next (t : Icc v.tMin v.tMax) :
    HasDerivWithinAt (f.next ∘ v.proj) (v t (f t)) (Icc v.tMin v.tMax) t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t))
    (Icc v.tMin v.tMax) ↑t

Tactic:
refine HasDerivWithinAt.const_add _ ?_

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax)
    ↑t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (f.vComp ↑t) (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax)
    ↑t

Tactic:
rw [vComp_apply_coe] at this

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax)
    ↑t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
⊢ HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax)
    ↑t

Tactic:
refine this.congr_of_eventuallyEq_of_mem ?_ t.coe_prop

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
⊢ (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x =>
    ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
a✝ : ℝ
ht' : a✝ ∈ Icc v.tMin v.tMax
⊢ ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj a✝), f.vComp τ = ∫ (τ : ℝ) in ↑v.t₀..a✝, f.vComp τ

Tactic:
rw [v.proj_of_mem ht']

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t

Tactic:
simp only [Function.comp_def, next_apply]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t))
    (Icc v.tMin v.tMax) ↑t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
⊢ (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x =>
    ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ht'

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
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, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
a✝ : ℝ
ht' : a✝ ∈ Icc v.tMin v.tMax
⊢ ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj a✝), f.vComp τ = ∫ (τ : ℝ) in ↑v.t₀..a✝, f.vComp τ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t

Tactic:
haveI : Fact ((t : ℝ) ∈ Icc v.tMin v.tMax) := ⟨t.2⟩

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
inst✝ : CompleteSpace E
t : ↑(Icc v.tMin v.tMax)
this : Fact (↑t ∈ Icc v.tMin v.tMax)
⊢ HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t