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])
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ N K, ContractingWith K (FunSpace.next^[N])
rcases ((Real.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually
  (gt_mem_nhds zero_lt_one)).exists with ⟨N, hN⟩
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])
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])
have : (0 : ℝ) ≤ (v.L * v.tDist) ^ N / N ! :=
  div_nonneg (pow_nonneg (mul_nonneg v.L.2 v.tDist_nonneg) _) (Nat.cast_nonneg _)
no goals
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])
exact ⟨N, ⟨_, this⟩, hN, LipschitzWith.of_dist_le_mul fun f g =>
  FunSpace.dist_iterate_next_le f g N⟩