[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ ↑{ val := 0, property := (_ : 0 ≤ 0 ∧ 0 ≤ 0) } ∈ Icc 0 0
[PROOFSTEP]
rw [Subtype.coe_mk, Icc_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ 0 ∈ {0}
[PROOFSTEP]
exact mem_singleton _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
x✝¹ : E
x✝ : x✝¹ ∈ closedBall 0 ↑0
⊢ ContinuousOn (fun t => OfNat.ofNat 0 t x✝¹) (Icc 0 0)
[PROOFSTEP]
simpa only [Pi.zero_apply] using continuousOn_const
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ dist t v.t₀ ≤ tDist v
[PROOFSTEP]
rw [Subtype.dist_eq, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
cases' le_total t v.t₀ with ht ht
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
rw [abs_of_nonpos (sub_nonpos.2 <| Subtype.coe_le_coe.2 ht), neg_sub]
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : t ≤ v.t₀
⊢ ↑v.t₀ - ↑t ≤ tDist v
[PROOFSTEP]
exact (sub_le_sub_left t.2.1 _).trans (le_max_right _ _)
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ |↑t - ↑v.t₀| ≤ tDist v
[PROOFSTEP]
rw [abs_of_nonneg (sub_nonneg.2 <| Subtype.coe_le_coe.2 ht)]
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
ht : v.t₀ ≤ t
⊢ ↑t - ↑v.t₀ ≤ tDist v
[PROOFSTEP]
exact (sub_le_sub_right t.2.2 _).trans (le_max_left _ _)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ ↑(proj v t) = t
[PROOFSTEP]
simp only [proj, projIcc_of_mem v.tMin_le_tMax ht]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ f g : FunSpace v
h : (fun f => ContinuousMap.mk f.toFun) f = (fun f => ContinuousMap.mk f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f g : FunSpace v
toFun✝ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝ : toFun✝ v.t₀ = v.x₀
lipschitz'✝ : LipschitzWith v.C toFun✝
h :
  (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ } =
    (fun f => ContinuousMap.mk f.toFun) g
⊢ { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
toFun✝¹ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝¹ : toFun✝¹ v.t₀ = v.x₀
lipschitz'✝¹ : LipschitzWith v.C toFun✝¹
toFun✝ : ↑(Icc v.tMin v.tMax) → E
map_t₀'✝ : toFun✝ v.t₀ = v.x₀
lipschitz'✝ : LipschitzWith v.C toFun✝
h :
  (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝¹, map_t₀' := map_t₀'✝¹, lipschitz' := lipschitz'✝¹ } =
    (fun f => ContinuousMap.mk f.toFun) { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ }
⊢ { toFun := toFun✝¹, map_t₀' := map_t₀'✝¹, lipschitz' := lipschitz'✝¹ } =
    { toFun := toFun✝, map_t₀' := map_t₀'✝, lipschitz' := lipschitz'✝ }
[PROOFSTEP]
simpa using h
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ range ↑toContinuousMap = {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
ext f
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap ↔ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap → f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
rintro ⟨⟨f, hf₀, hf_lip⟩, rfl⟩
[GOAL]
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ ↑toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
[PROOFSTEP]
exact ⟨hf₀, hf_lip⟩
[GOAL]
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → f ∈ range ↑toContinuousMap
[PROOFSTEP]
rcases f with ⟨f, hf⟩
[GOAL]
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ ContinuousMap.mk f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → ContinuousMap.mk f ∈ range ↑toContinuousMap
[PROOFSTEP]
rintro ⟨hf₀, hf_lip⟩
[GOAL]
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : ↑(ContinuousMap.mk f) v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ↑(ContinuousMap.mk f)
⊢ ContinuousMap.mk f ∈ range ↑toContinuousMap
[PROOFSTEP]
exact ⟨⟨f, hf₀, hf_lip⟩, rfl⟩
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun f t) v.x₀ = dist (toFun f t) (toFun f v.t₀)
[PROOFSTEP]
rw [f.map_t₀']
[GOAL]
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)
[PROOFSTEP]
simp only [vComp, proj_coe]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ Continuous (vComp f)
[PROOFSTEP]
have := (continuous_subtype_val.prod_mk f.continuous).comp v.continuous_proj
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
⊢ Continuous (vComp f)
[PROOFSTEP]
refine' ContinuousOn.comp_continuous v.continuousOn this fun x => _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
x : ℝ
⊢ ((fun x => (↑x, toFun f x)) ∘ proj v) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R
[PROOFSTEP]
exact ⟨(v.proj x).2, f.mem_closedBall _⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ CompleteSpace (FunSpace v)
[PROOFSTEP]
refine' (completeSpace_iff_isComplete_range uniformInducing_toContinuousMap).2 (IsClosed.isComplete _)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed (range ↑toContinuousMap)
[PROOFSTEP]
rw [range_toContinuousMap, setOf_and]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed ({a | ↑a v.t₀ = v.x₀} ∩ {a | LipschitzWith v.C ↑a})
[PROOFSTEP]
refine' (isClosed_eq (ContinuousMap.continuous_eval_const _) continuous_const).inter _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
⊢ IsClosed {a | LipschitzWith v.C ↑a}
[PROOFSTEP]
have : IsClosed {f : Icc v.tMin v.tMax → E | LipschitzWith v.C f} := isClosed_setOf_lipschitzWith v.C
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
this : IsClosed {f | LipschitzWith v.C f}
⊢ IsClosed {a | LipschitzWith v.C ↑a}
[PROOFSTEP]
exact this.preimage ContinuousMap.continuous_coe
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
⊢ (fun t => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t, vComp f τ) v.t₀ = v.x₀
[PROOFSTEP]
simp only [integral_same, add_zero]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
t₁ t₂ : ↑(Icc v.tMin v.tMax)
⊢ dist (v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t₁, vComp f τ) (v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t₂, vComp f τ) ≤ ↑v.C * dist t₁ t₂
[PROOFSTEP]
rw [dist_add_left, dist_eq_norm,
  integral_interval_sub_left (f.intervalIntegrable_vComp _ _) (f.intervalIntegrable_vComp _ _)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
inst✝ : CompleteSpace E
f : FunSpace v
t₁ t₂ : ↑(Icc v.tMin v.tMax)
⊢ ‖∫ (x : ℝ) in ↑t₂..↑t₁, vComp f x‖ ≤ ↑v.C * dist t₁ t₂
[PROOFSTEP]
exact norm_integral_le_of_norm_le_const fun t _ => f.norm_vComp_le _
[GOAL]
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
[PROOFSTEP]
haveI : Fact ((t : ℝ) ∈ Icc v.tMin v.tMax) := ⟨t.2⟩
[GOAL]
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
[PROOFSTEP]
simp only [(· ∘ ·), next_apply]
[GOAL]
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
[PROOFSTEP]
refine' HasDerivWithinAt.const_add _ _
[GOAL]
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
[PROOFSTEP]
have : HasDerivWithinAt (∫ τ in v.t₀..·, f.vComp τ) (f.vComp t) (Icc v.tMin v.tMax) t :=
  integral_hasDerivWithinAt_right (f.intervalIntegrable_vComp _ _) (f.continuous_vComp.stronglyMeasurableAtFilter _ _)
    f.continuous_vComp.continuousWithinAt
[GOAL]
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
[PROOFSTEP]
rw [vComp_apply_coe] at this 
[GOAL]
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
[PROOFSTEP]
refine' this.congr_of_eventuallyEq_of_mem _ t.coe_prop
[GOAL]
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 τ
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with _ ht'
[GOAL]
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 τ
[PROOFSTEP]
rw [v.proj_of_mem ht']
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
h : ∀ (t : ↑(Icc v.tMin v.tMax)), dist (toFun f₁ t) (toFun f₂ t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next f₁) t) (toFun (next f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
simp only [dist_eq_norm, next_apply, add_sub_add_left_eq_sub, ←
  intervalIntegral.integral_sub (intervalIntegrable_vComp _ _ _) (intervalIntegrable_vComp _ _ _),
  norm_integral_eq_norm_integral_Ioc] at *
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (x : ℝ) in Ι ↑v.t₀ ↑t, vComp f₁ x - vComp f₂ x‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
calc
  ‖∫ τ in Ι (v.t₀ : ℝ) t, f₁.vComp τ - f₂.vComp τ‖ ≤ ∫ τ in Ι (v.t₀ : ℝ) t, v.L * ((v.L * |τ - v.t₀|) ^ n / n ! * d) :=
    by
    refine' norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc _) _
    ·
      -- porting note: was `continuity`
      refine .mul continuous_const <| .mul (.div_const ?_ _) continuous_const
      refine .pow (.mul continuous_const <| .abs <| ?_) _
      exact .sub continuous_id continuous_const
    · refine' (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ => _
      refine'
        (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _) (f₂.mem_closedBall _)
          ((h _).trans_eq _)
      rw [v.proj_of_mem]
      exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ
  _ = (v.L * |t.1 - v.t₀|) ^ (n + 1) / (n + 1)! * d := by
    simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left, MeasureTheory.integral_mul_right,
      integral_pow_abs_sub_uIoc, div_eq_mul_inv, pow_succ (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ,
      mul_inv, mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, vComp f₁ τ - vComp f₂ τ‖ ≤
    ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine' norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc _) _
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine .mul continuous_const <| .mul (.div_const ?_ _) continuous_const
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => (↑v.L * |τ - ↑v.t₀|) ^ n
[PROOFSTEP]
refine .pow (.mul continuous_const <| .abs <| ?_) _
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => τ - ↑v.t₀
[PROOFSTEP]
exact .sub continuous_id continuous_const
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι ↑v.t₀ ↑t),
    ‖vComp f₁ x - vComp f₂ x‖ ≤ ↑v.L * ((↑v.L * |x - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine' (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ => _
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ ‖vComp f₁ τ - vComp f₂ τ‖ ≤ ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)
[PROOFSTEP]
refine'
  (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _) (f₂.mem_closedBall _) ((h _).trans_eq _)
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ (↑v.L * |↑(proj v τ) - ↑v.t₀|) ^ n / ↑n ! * d = (↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d
[PROOFSTEP]
rw [v.proj_of_mem]
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (min ↑v.t₀ ↑t) (max ↑v.t₀ ↑t)
⊢ τ ∈ Icc v.tMin v.tMax
[PROOFSTEP]
exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖toFun f₁ t - toFun f₂ t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d) =
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
[PROOFSTEP]
simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left, MeasureTheory.integral_mul_right,
  integral_pow_abs_sub_uIoc, div_eq_mul_inv, pow_succ (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ,
  mul_inv, mul_assoc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
induction' n with n ihn generalizing t
[GOAL]
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[Nat.zero] f₁) t) (toFun (next^[Nat.zero] f₂) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.zero / ↑Nat.zero ! * dist f₁ f₂
[PROOFSTEP]
rw [Nat.zero_eq, pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul]
[GOAL]
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[0] f₁) t) (toFun (next^[0] f₂) t) ≤ dist f₁ f₂
[PROOFSTEP]
exact dist_apply_le_dist f₁ f₂ t
[GOAL]
case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ : ↑(Icc v.tMin v.tMax)
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next^[Nat.succ n] f₁) t) (toFun (next^[Nat.succ n] f₂) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
[PROOFSTEP]
rw [iterate_succ_apply', iterate_succ_apply']
[GOAL]
case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
t✝ : ↑(Icc v.tMin v.tMax)
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist (toFun (next^[n] f₁) t) (toFun (next^[n] f₂) t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist (toFun (next (next^[n] f₁)) t) (toFun (next (next^[n] f₂)) t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
[PROOFSTEP]
exact dist_next_apply_le_of_le ihn _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
⊢ dist (next^[n] f₁) (next^[n] f₂) ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
refine' dist_le_of_forall fun t => (dist_iterate_next_apply_le _ _ _ _).trans _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
have : |(t - v.t₀ : ℝ)| ≤ v.tDist := v.dist_t₀_le t
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : |↑t - ↑v.t₀| ≤ tDist v
⊢ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
[PROOFSTEP]
gcongr
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
rcases((Real.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually (gt_mem_nhds zero_lt_one)).exists with ⟨N, hN⟩
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
N : ℕ
hN : (↑v.L * tDist v) ^ N / ↑N ! < 1
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
have : (0 : ℝ) ≤ (v.L * v.tDist) ^ N / N ! :=
  div_nonneg (pow_nonneg (mul_nonneg v.L.2 v.tDist_nonneg) _) (Nat.cast_nonneg _)
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
N : ℕ
hN : (↑v.L * tDist v) ^ N / ↑N ! < 1
this : 0 ≤ (↑v.L * tDist v) ^ N / ↑N !
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
[PROOFSTEP]
exact ⟨N, ⟨_, this⟩, hN, LipschitzWith.of_dist_le_mul fun f g => FunSpace.dist_iterate_next_le f g N⟩
[GOAL]
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
[PROOFSTEP]
rcases v.exists_fixed with ⟨f, hf⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨f ∘ v.proj, _, fun t ht => _⟩
[GOAL]
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₀
[PROOFSTEP]
simp only [(· ∘ ·), proj_coe, f.map_t₀]
[GOAL]
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
[PROOFSTEP]
simp only [(· ∘ ·), v.proj_of_mem ht]
[GOAL]
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
[PROOFSTEP]
lift t to Icc v.tMin v.tMax using ht
[GOAL]
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
[PROOFSTEP]
simpa only [hf, v.proj_coe] using f.hasDerivWithinAt_next t
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
C R : ℝ
L : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
lift C to ℝ≥0 using (norm_nonneg _).trans hpl.norm_le₀
[GOAL]
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R ↑C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
lift t₀ to Icc tMin tMax using hpl.ht₀
[GOAL]
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
t₀ : { x // x ∈ Icc tMin tMax }
hpl : IsPicardLindelof v tMin (↑t₀) tMax x₀ L R ↑C
⊢ ∃ f, f ↑t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Icc tMin tMax → HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
[PROOFSTEP]
exact PicardLindelof.exists_solution ⟨v, tMin, tMax, t₀, x₀, C, ⟨R, hpl.hR⟩, L, { hpl with ht₀ := t₀.property }⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨L, s', hs', hlip⟩ :=
  ContDiffAt.exists_lipschitzOnWith
    ((hv.contDiffWithinAt (mem_of_mem_nhds hs)).contDiffAt hs)
      -- radius of closed ball in which v is bounded
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨r, hr : 0 < r, hball⟩ := Metric.mem_nhds_iff.mp (inter_sets (𝓝 x₀) hs hs')
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hr' := (half_pos hr).le
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
obtain ⟨C, hC⟩ :=
  (isCompact_closedBall x₀ (r / 2)).bddAbove_image <|
    hv.continuousOn.norm.mono (subset_inter_iff.mp ((closedBall_subset_ball (half_lt_self hr)).trans hball)).left
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hC' : 0 ≤ C := by
  apply (norm_nonneg (v x₀)).trans
  apply hC
  exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ 0 ≤ C
[PROOFSTEP]
apply (norm_nonneg (v x₀)).trans
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ≤ C
[PROOFSTEP]
apply hC
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ∈ (fun x => ‖v x‖) '' closedBall x₀ (r / 2)
[PROOFSTEP]
exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
set ε := if C = 0 then 1 else r / 2 / C with hε
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
have hε0 : 0 < ε := by
  rw [hε]
  split_ifs with h
  · exact zero_lt_one
  · exact div_pos (half_pos hr) (lt_of_le_of_ne hC' (Ne.symm h))
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < ε
[PROOFSTEP]
rw [hε]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < if C = 0 then 1 else r / 2 / C
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : C = 0
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : ¬C = 0
⊢ 0 < r / 2 / C
[PROOFSTEP]
exact div_pos (half_pos hr) (lt_of_le_of_ne hC' (Ne.symm h))
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
[PROOFSTEP]
refine' ⟨ε, hε0, L, r / 2, C, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L (r / 2) C
[PROOFSTEP]
exact
  { ht₀ := by rw [← Real.closedBall_eq_Icc]; exact mem_closedBall_self hε0.le
    hR := (half_pos hr).le
    lipschitz := fun t _ =>
      hlip.mono (subset_inter_iff.mp (Subset.trans (closedBall_subset_ball (half_lt_self hr)) hball)).2
    cont := fun x _ => continuousOn_const
    norm_le := fun t _ x hx => hC ⟨x, hx, rfl⟩
    C_mul_le_R := by
      rw [add_sub_cancel', sub_sub_cancel, max_self, mul_ite, mul_one]
      split_ifs with h
      · rwa [← h] at hr' 
      · exact (mul_div_cancel' (r / 2) h).le }
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)
[PROOFSTEP]
rw [← Real.closedBall_eq_Icc]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ closedBall t₀ ε
[PROOFSTEP]
exact mem_closedBall_self hε0.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ C * max (t₀ + ε - t₀) (t₀ - (t₀ - ε)) ≤ r / 2
[PROOFSTEP]
rw [add_sub_cancel', sub_sub_cancel, max_self, mul_ite, mul_one]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ (if C = 0 then C else C * (r / 2 / C)) ≤ r / 2
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : C = 0
⊢ C ≤ r / 2
[PROOFSTEP]
rwa [← h] at hr' 
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : ¬C = 0
⊢ C * (r / 2 / C) ≤ r / 2
[PROOFSTEP]
exact (mul_div_cancel' (r / 2) h).le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨ε, hε, L, R, C, hpl⟩ := exists_isPicardLindelof_const_of_contDiffOn_nhds t₀ x₀ hv hs
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨f, hf1, hf2⟩ := hpl.exists_forall_hasDerivWithinAt_Icc_eq x₀
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
have hf2' : ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t := fun t ht =>
  (hf2 t (Ioo_subset_Icc_self ht)).hasDerivAt (Icc_mem_nhds ht.1 ht.2)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
have h : f ⁻¹' s ∈ 𝓝 t₀ :=
  by
  have := hf2' t₀ (mem_Ioo.mpr ⟨sub_lt_self _ hε, lt_add_of_pos_right _ hε⟩)
  apply ContinuousAt.preimage_mem_nhds this.continuousAt
  rw [hf1]
  exact hs
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
⊢ f ⁻¹' s ∈ 𝓝 t₀
[PROOFSTEP]
have := hf2' t₀ (mem_Ioo.mpr ⟨sub_lt_self _ hε, lt_add_of_pos_right _ hε⟩)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ f ⁻¹' s ∈ 𝓝 t₀
[PROOFSTEP]
apply ContinuousAt.preimage_mem_nhds this.continuousAt
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ s ∈ 𝓝 (f t₀)
[PROOFSTEP]
rw [hf1]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
this : HasDerivAt f (v (f t₀)) t₀
⊢ s ∈ 𝓝 x₀
[PROOFSTEP]
exact hs
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
h : f ⁻¹' s ∈ 𝓝 t₀
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
rw [Metric.mem_nhds_iff] at h 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
h : ∃ ε, ε > 0 ∧ ball t₀ ε ⊆ f ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
obtain ⟨r, hr1, hr2⟩ := h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∃ f, f t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → f t ∈ s ∧ HasDerivAt f (v (f t)) t
[PROOFSTEP]
refine
  ⟨min r ε, lt_min hr1 hε, f, hf1, fun t ht =>
    ⟨?_,
      hf2' t
        (mem_of_mem_of_subset ht
          (Ioo_subset_Ioo (sub_le_sub_left (min_le_right _ _) _) (add_le_add_left (min_le_right _ _) _)))⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ f t ∈ s
[PROOFSTEP]
rw [← Set.mem_preimage]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ t ∈ f ⁻¹' s
[PROOFSTEP]
apply Set.mem_of_mem_of_subset _ hr2
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ t ∈ ball t₀ r
[PROOFSTEP]
apply Set.mem_of_mem_of_subset ht
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ Ioo (t₀ - min r ε) (t₀ + min r ε) ⊆ ball t₀ r
[PROOFSTEP]
rw [← Real.ball_eq_Ioo]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
ε : ℝ
hε : ε > 0
L : ℝ≥0
R C : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ (t : ℝ), t ∈ Icc (t₀ - ε) (t₀ + ε) → HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
hf2' : ∀ (t : ℝ), t ∈ Ioo (t₀ - ε) (t₀ + ε) → HasDerivAt f (v (f t)) t
r : ℝ
hr1 : r > 0
hr2 : ball t₀ r ⊆ f ⁻¹' s
t : ℝ
ht : t ∈ Ioo (t₀ - min r ε) (t₀ + min r ε)
⊢ ball t₀ (min r ε) ⊆ ball t₀ r
[PROOFSTEP]
exact Metric.ball_subset_ball (min_le_left _ _)
