awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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)
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
⊢ dist (next hf hx α) (next hf hy α) = dist x y

Tactic:
rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq, dist_eq_norm, ContinuousMap.norm_eq_iSup_norm]

Premises used: ODE.FunSpace.toContinuousMap, dist_eq_norm, ContinuousMap.norm_eq_iSup_norm, Isometry.dist_eq, Function.Embedding.injective, MetricSpace.isometry_induced, DFunLike.coe
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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)
⊢ ⨆ (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:
simp [add_sub_add_right_eq_sub, dist_eq_norm]

Premises used: dist_eq_norm, add_sub_add_right_eq_sub
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ dist α ((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) α]

Premises used: ODE.FunSpace.next, Function.iterate_zero_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ 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]

Premises used: Finset.sum_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ 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:
apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[i] α)

Premises used: dist_le_range_sum_of_dist_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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 α)
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i + 1] α) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)

Tactic:
rw [iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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] (next hf hx α)) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)

Tactic:
dist_iterate_next_iterate_next_le hf hx _ _ i

Premises used: ODE.FunSpace.dist_iterate_next_iterate_next_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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] (next hf hx α)) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ) * dist α (next hf hx α)

Tactic:
exact dist_iterate_next_iterate_next_le hf hx _ _ i

Premises used: ODE.FunSpace.dist_iterate_next_iterate_next_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ 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 α)

Tactic:
nth_rw 1 [← iterate_zero_apply (next hf hx) α]

Premises used: ODE.FunSpace.next, Function.iterate_zero_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ 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:
rw [Finset.mul_sum, Finset.sum_mul]

Premises used: Finset.mul_sum, Finset.sum_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ
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 α)
⊢ 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:
apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[m]^[i] α)

Premises used: dist_le_range_sum_of_dist_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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 α)
⊢ 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 α)

Tactic:
rw [iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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 α)
⊢ 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:
apply le_trans <| hm.dist_iterate_succ_le_geometric α i

Premises used: LipschitzWith.dist_iterate_succ_le_geometric, le_trans
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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
⊢ 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:
rw [mul_assoc, mul_comm ((C : ℝ) ^ i), ← mul_assoc]

Premises used: mul_assoc, HPow.hPow, mul_comm, NNReal.toReal
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
hd :
  dist α ((next hf hx)^[m] α) ≤
    (∑ i ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α)
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α)

Tactic:
dist_iterate_next_le hf hx α m

Premises used: ODE.FunSpace.dist_iterate_next_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 ∈ Finset.range m, ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ i / (↑i ! : ℝ)) *
      dist α (next hf hx α)

Tactic:
exact dist_iterate_next_le hf hx α m

Premises used: ODE.FunSpace.dist_iterate_next_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
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
⊢ ∃ (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

Premises used: ODE.FunSpace.exists_contractingWith_iterate_next
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 ≤ 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
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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)⁻¹ : ℝ)
this : 0 ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ 0 ≤ L'

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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'

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
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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

Tactic:
⟨.mk L' hL', fun x y hx hy α β hα hβ ↦ ?_⟩

Premises used: NNReal.mk, Exists.intro
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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'
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
⊢ ∃ (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:
refine ⟨.mk L' hL', fun x y hx hy α β hα hβ ↦ ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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) β
rw : dist α β ≤ L' * dist x y
⊢ dist α β ≤ (↑(NNReal.mk L' hL') : ℝ) * dist x y

Tactic:
rw [NNReal.coe_mk]

Premises used: NNReal.coe_mk
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 α β))
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))
⊢ dist α β ≤ 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

Premises used: ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith, And.right, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 β)
⊢ Filter.Tendsto (fun (x : ℕ) ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))

Tactic:
apply Filter.Tendsto.comp (y := 𝓝 β) (tendsto_const_nhds.dist Filter.tendsto_id)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.dist, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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) β
rw :
  Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 (ContractingWith.fixedPoint (next hf hy)^[m] ⋯))
⊢ Filter.Tendsto (fun (x : ℕ) ↦ (next hf hy)^[m]^[x] α) Filter.atTop (𝓝 β)

Tactic:
rw [h y hy |>.fixedPoint_unique (hβ.iterate m)]

Premises used: Function.IsFixedPt.iterate, ContractingWith.fixedPoint_unique
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 (𝓝 (ContractingWith.fixedPoint (next hf hy)^[m] ⋯))

Tactic:
h y hy |>.tendsto_iterate_fixedPoint α

Premises used: ContractingWith.tendsto_iterate_fixedPoint