awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mp : IsFixedPt (next hf hx) α → ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
⊢ IsFixedPt (next hf hx) α ↔ ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
have mpr : (∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)) → IsFixedPt (next hf hx) α
Tactic: constructor
-- 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
h : ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
⊢ IsFixedPt (next hf hx) α
have mpr : ∀ (t : (↑(Icc tmin tmax) : Type)), (next hf hx α).toFun t = α.toFun t
Tactic: ext 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 : 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
h : ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ (next hf hx α).toFun t = α.toFun t
have mpr : (next hf hx α).toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
Tactic: rw [h, next_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
h : ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
t : (↑(Icc tmin tmax) : Type)
mpr : (next hf hx α).toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
⊢ (next hf hx α).toFun t = α.toFun t
have mpr₁ : picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ) = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
Tactic: rw [h, next_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 : ℝ)
n : ℕ
t : (↑(Icc tmin tmax) : Type)
α β : FunSpace t₀ x₀ r L
h :
  dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
⊢ (↑K : ℝ) * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    (↑K : ℝ) ^ (n + 1) * |(↑t : ℝ) - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have rw : (↑K : ℝ) * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
  (↑K : ℝ) * ((↑K : ℝ) ^ n * |(↑t : ℝ) - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β)
Tactic: rw [pow_succ', mul_assoc, mul_div_assoc, 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 : ℝ)
n : ℕ
t : (↑(Icc tmin tmax) : Type)
α β : FunSpace t₀ x₀ r L
h :
  dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
⊢ (↑K : ℝ) * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    (↑K : ℝ) * ((↑K : ℝ) ^ n * |(↑t : ℝ) - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β)
have hbc : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
  (↑K : ℝ) ^ n * |(↑t : ℝ) - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
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₀ 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ dist (((next hf hx)^[n + 1] α).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have succ : norm.{u_1} (E := E)
    (∫ (x_1 : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ),
      f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)) ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [iterate_succ_apply', iterate_succ_apply', dist_eq_norm, next_apply,
      next_apply, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      ← intervalIntegral.integral_sub (intervalIntegrable_comp_compProj hf _ t)
        (intervalIntegrable_comp_compProj hf _ 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 : 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ norm.{u_1} (E := E)
      (∫ (x_1 : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ),
        f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
      (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have rw : norm.{u_1} (E := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (x_1 : ℝ) ↦
      f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)) ≤
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
    (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
Tactic: rw [intervalIntegral.norm_intervalIntegral_eq]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (x_1 : ℝ) ↦
        f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
      (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have apply : ∀ᵐ (x_1 : ℝ) ∂Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ)),
  ‖f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)‖ ≤
    (↑K : ℝ) ^ (n + 1) * |x_1 - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
Tactic: apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ ∀ᵐ (x_1 : ℝ) ∂Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ)),
    ‖f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)‖ ≤
      (↑K : ℝ) ^ (n + 1) * |x_1 - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have apply : ∀ x_1 ∈ Ioc (min (↑t₀ : ℝ) (↑t : ℝ)) (max (↑t₀ : ℝ) (↑t : ℝ)),
  ‖f x_1 (((next hf hx)^[n] α).compProj x_1) - f x_1 (((next hf hx)^[n] β).compProj x_1)‖ ≤
    (↑K : ℝ) ^ (n + 1) * |x_1 - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
Tactic: apply ae_restrict_mem measurableSet_Ioc |>.mono
-- 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 : 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
t' : ℝ
ht' : t' ∈ Ioc (min (↑t₀ : ℝ) (↑t : ℝ)) (max (↑t₀ : ℝ) (↑t : ℝ))
⊢ ‖f t' (((next hf hx)^[n] α).compProj t') - f t' (((next hf hx)^[n] β).compProj t')‖ ≤
    (↑K : ℝ) ^ (n + 1) * |t' - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have ht'₁ : t' ∈ Icc tmin tmax
Tactic: have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
t' : ℝ
ht'_1 : t' ∈ Ioc (min (↑t₀ : ℝ) (↑t : ℝ)) (max (↑t₀ : ℝ) (↑t : ℝ))
ht' : t' ∈ Icc tmin tmax
⊢ ‖f t' (((next hf hx)^[n] α).compProj t') - f t' (((next hf hx)^[n] β).compProj t')‖ ≤
    (↑K : ℝ) ^ (n + 1) * |t' - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
have rw : dist (f t' (((next hf hx)^[n] α).toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht')))
    (f t' (((next hf hx)^[n] β).toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht'))) ≤
  (↑K : ℝ) ^ (n + 1) * |t' - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β
Tactic: rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
      (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h : |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
      (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: apply le_of_abs_le
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h : |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
h :
  |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h₁ : |(∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ)) * dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
h :
  |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₁ :
  |(∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ)) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h₂ : |HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n) (↑n ! : ℝ) *
      dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
h :
  |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₁ :
  |(∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ)) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₂ :
  |HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n) (↑n ! : ℝ) *
        dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h₃ : |((↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n) / (↑n ! : ℝ) * dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
h :
  |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₁ :
  |(∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ)) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₂ :
  |HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n) (↑n ! : ℝ) *
        dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₃ :
  |((↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n) / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h₄ : |((↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n) / (↑n ! : ℝ)| * |dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]
-- 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 : ℕ
hn :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
      ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
t : (↑(Icc tmin tmax) : Type)
h :
  |∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₁ :
  |(∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ)) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₂ :
  |HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n) (↑n ! : ℝ) *
        dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₃ :
  |((↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n) / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
h₄ :
  |((↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n) / (↑n ! : ℝ)| * |dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
⊢ |@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (τ : ℝ) ↦
        (↑K : ℝ) ^ (n + 1) * |τ - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β| ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
have h₅ : |(↑K : ℝ) ^ (n + 1) * ∫ (x : ℝ) in (↑t₀ : ℝ)..(↑t : ℝ), |x - (↑t₀ : ℝ)| ^ n| / |(↑n ! : ℝ)| * |dist α β| ≤
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ (n + 1) / (↑(n + 1)! : ℝ) * dist α β
Tactic: rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]