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 * abs (↑t - ↑v.t₀)) ^ Nat.zero / ↑Nat.zero ! * dist f₁ f₂

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 * abs (↑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 * abs (↑t - ↑v.t₀)) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
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 * abs (↑t - ↑v.t₀)) ^ n / ↑n ! * dist f₁ f₂
induction' n with n ihn generalizing t
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₂
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 * abs (↑t - ↑v.t₀)) ^ Nat.zero / ↑Nat.zero ! * dist f₁ f₂
rw [Nat.zero_eq, pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul]
no goals
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₂
exact dist_apply_le_dist f₁ f₂ t
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 * abs (↑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 * abs (↑t - ↑v.t₀)) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
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 * abs (↑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 * abs (↑t - ↑v.t₀)) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
rw [iterate_succ_apply', iterate_succ_apply']
no goals
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 * abs (↑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 * abs (↑t - ↑v.t₀)) ^ Nat.succ n / ↑(Nat.succ n)! * dist f₁ f₂
exact dist_next_apply_le_of_le ihn _