awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
n : ℕ
hn : ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) < 1
⊢ ∃ (n : ℕ) (C : ℝ≥0), ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[n]
have this : 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ)
Tactic: have : (0 : ℝ) ≤ (K * max (tmax - t₀) (t₀ - tmin)) ^ n / n ! := by
    have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
n : ℕ
hn : ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) < 1
this : 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ)
⊢ ∃ (n : ℕ) (C : ℝ≥0), ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[n]
have refine : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)),
  ContractingWith
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ))
      this)
    (next hf hx)^[n]
Tactic: refine ⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
⊢ dist (next hf hx α) (next hf hy α) = dist x y
have this : Nonempty (↑(Icc tmin tmax) : Type)
Tactic: have : Nonempty (Icc tmin tmax) := ⟨t₀⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
this : Nonempty (↑(Icc tmin tmax) : Type)
⊢ dist (next hf hx α) (next hf hy α) = dist x y
have rw : ⨆ (x_1 : (↑(Icc tmin tmax) : Type)),
    norm (E := E)
      ((HSub.hSub (α := C((↑(Icc tmin tmax) : Type), E)) (β := C((↑(Icc tmin tmax) : Type), E))
              ((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (next hf hx α) :
                C((↑(Icc tmin tmax) : Type), E))
              ((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (next hf hy α) :
                C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          x_1 :
        E) =
  dist x y
Tactic: rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq, dist_eq_norm, ContinuousMap.norm_eq_iSup_norm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist α ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α)
have nth_rw : dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
  (∑ i ∈ Finset.range n, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
    dist α (next hf hx α)
Tactic: nth_rw 1 [← iterate_zero_apply (next hf hx) α]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α)
have rw : dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
  ∑ i ∈ Finset.range n, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)
Tactic: rw [Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    ∑ i ∈ Finset.range n,
      ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)
have hd : ∀ {k : ℕ},
  k < n →
    dist ((next hf hx)^[k] α) ((next hf hx)^[k + 1] α) ≤
      ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ k / (↑k ! : ℝ) * dist α (next hf hx α)
Tactic: apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[i] α)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)
have hd : dist ((next hf hx)^[i] α) ((next hf hx)^[i] (next hf hx α)) ≤
  ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)
Tactic: rw [iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist α ((next hf hx)^[m]^[n] α) ≤
    HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range n, (↑C : ℝ) ^ i) *
      dist α (next hf hx α)
have nth_rw : dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
  HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
      (∑ i ∈ Finset.range n, (↑C : ℝ) ^ i) *
    dist α (next hf hx α)
Tactic: nth_rw 1 [← iterate_zero_apply (next hf hx) α]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range n, (↑C : ℝ) ^ i) *
      dist α (next hf hx α)
have rw : dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
  ∑ i ∈ Finset.range n,
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
      dist α (next hf hx α)
Tactic: rw [Finset.mul_sum, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ∑ i ∈ Finset.range n,
      (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
        dist α (next hf hx α)
have hd : ∀ {k : ℕ},
  k < n →
    dist ((next hf hx)^[m]^[k] α) ((next hf hx)^[m]^[k + 1] α) ≤
      (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ k *
        dist α (next hf hx α)
Tactic: apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[m]^[i] α)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i + 1] α) ≤
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
      dist α (next hf hx α)
have hd : dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i] ((next hf hx)^[m] α)) ≤
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
    dist α (next hf hx α)
Tactic: rw [iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i] ((next hf hx)^[m] α)) ≤
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
      dist α (next hf hx α)
have hd : dist α ((next hf hx)^[m] α) * (↑C : ℝ) ^ i ≤
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
    dist α (next hf hx α)
Tactic: apply le_trans <| hm.dist_iterate_succ_le_geometric α i
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * (↑C : ℝ) ^ i ≤
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑C : ℝ) ^ i *
      dist α (next hf hx α)
have hd : dist α ((next hf hx)^[m] α) * (↑C : ℝ) ^ i ≤
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α) *
    (↑C : ℝ) ^ i
Tactic: rw [mul_assoc, mul_comm ((C : ℝ) ^ i), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * (↑C : ℝ) ^ i ≤
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
        dist α (next hf hx α) *
      (↑C : ℝ) ^ i
have hd : dist α ((next hf hx)^[m] α) ≤
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
    dist α (next hf hx α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
⊢ ∃ (L' : ℝ≥0),
    ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
      IsFixedPt (next hf hx) α → IsFixedPt (next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
have obtain : ∀ (m : ℕ) (C : ℝ≥0) (h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]),
  ∃ (L' : ℝ≥0),
    ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
      IsFixedPt (next hf hx) α → IsFixedPt (next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
Tactic: obtain ⟨m, C, h⟩ := exists_contractingWith_iterate_next hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
⊢ 0 ≤ L'
have this : 0 ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
Tactic: have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
⊢ ∃ (L' : ℝ≥0),
    ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
      IsFixedPt (next hf hx) α → IsFixedPt (next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
have hL' : 0 ≤ L'
Tactic: have hL' : 0 ≤ L' := by
    have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
⊢ ∃ (L' : ℝ≥0),
    ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
      IsFixedPt (next hf hx) α → IsFixedPt (next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
have refine : ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L)
  (hα : IsFixedPt (next hf hx) α) (hβ : IsFixedPt (next hf hy) β), dist α β ≤ (↑(NNReal.mk L' hL') : ℝ) * dist x y
Tactic: refine ⟨.mk L' hL', fun x y hx hy α β hα hβ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ dist α β ≤ (↑(NNReal.mk L' hL') : ℝ) * dist x y
have rw : dist α β ≤ L' * dist x y
Tactic: rw [NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ dist α β ≤ L' * dist x y
have apply : Filter.Tendsto (fun (x : ℕ) ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))
Tactic: apply le_of_tendsto_of_tendsto' (b := Filter.atTop) _ _ <|
    dist_iterate_iterate_next_le_of_lipschitzWith hf hy α (h y hy).2
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
apply : Filter.Tendsto (fun (x : ℕ) ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))
⊢ dist α β ≤ L' * dist x y
have apply₁ : Filter.Tendsto
  (fun (x : ℕ) ↦
    HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) *
      dist α (next hf hy α))
  Filter.atTop (𝓝 (L' * dist x y))
Tactic: apply le_of_tendsto_of_tendsto' (b := Filter.atTop) _ _ <|
    dist_iterate_iterate_next_le_of_lipschitzWith hf hy α (h y hy).2
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun (x : ℕ) ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))
have apply : Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 β)
Tactic: apply Filter.Tendsto.comp (y := 𝓝 β) (tendsto_const_nhds.dist Filter.tendsto_id)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 β)
have rw : Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 (ContractingWith.fixedPoint (next hf hy)^[m] sorry))
Tactic: rw [h y hy |>.fixedPoint_unique (hβ.iterate m)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto
    (fun (x : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
          (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) *
        dist α (next hf hy α))
    Filter.atTop (𝓝 (L' * dist x y))
have nth_rw : Filter.Tendsto
  (fun (x_1 : ℕ) ↦
    HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range x_1, (↑C : ℝ) ^ i) *
      dist x y)
  Filter.atTop (𝓝 (L' * dist x y))
Tactic: nth_rw 1 [← hα, dist_next_next]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto
    (fun (x_1 : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
          (∑ i ∈ Finset.range x_1, (↑C : ℝ) ^ i) *
        dist x y)
    Filter.atTop (𝓝 (L' * dist x y))
have hf₁ : Filter.Tendsto
  (fun (x : ℕ) ↦
    HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
      (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i))
  Filter.atTop (𝓝 L')
Tactic: apply Filter.Tendsto.mul_const
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[m]
L' : ℝ :=
  (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) * (↑(1 - C)⁻¹ : ℝ)
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
hy : y ∈ closedBall x₀ (↑r : ℝ)
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto
    (fun (x : ℕ) ↦
      HMul.hMul (α := ℝ) (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ))
        (∑ i ∈ Finset.range x, (↑C : ℝ) ^ i))
    Filter.atTop (𝓝 L')
have hf₁ : Filter.Tendsto (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, (↑C : ℝ) ^ i) Filter.atTop (𝓝 (↑(1 - C)⁻¹ : ℝ))
Tactic: apply Filter.Tendsto.const_mul