E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ abs (↑t - ↑v.t₀) ≤ tDist v
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
rw [Subtype.dist_eq, Real.dist_eq]
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₀
⊢ abs (↑t - ↑v.t₀) ≤ tDist v

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
⊢ abs (↑t - ↑v.t₀) ≤ tDist v
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ↑(Icc v.tMin v.tMax)
⊢ abs (↑t - ↑v.t₀) ≤ tDist v
cases' le_total t v.t₀ with ht ht
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
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₀
⊢ abs (↑t - ↑v.t₀) ≤ tDist v
rw [abs_of_nonpos (sub_nonpos.2 <| Subtype.coe_le_coe.2 ht), neg_sub]
no goals
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
exact (sub_le_sub_left t.2.1 _).trans (le_max_right _ _)
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
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
⊢ abs (↑t - ↑v.t₀) ≤ tDist v
rw [abs_of_nonneg (sub_nonneg.2 <| Subtype.coe_le_coe.2 ht)]
no goals
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
exact (sub_le_sub_right t.2.2 _).trans (le_max_left _ _)