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
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 α β
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 α β
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)| *
        |@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (x : ℝ) ↦
            |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 α β
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 α β
h₇ :
  |(↑K : ℝ) ^ (n + 1)| *
          |@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (uIoc (↑t₀ : ℝ) (↑t : ℝ))) fun (x : ℝ) ↦
              |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)| * ||(↑t : ℝ) - (↑t₀ : ℝ)| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| / |(↑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)
⊢ 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 α β
have _ : 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 α β
Tactic: calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        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)
_ :
  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 α β
⊢ 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 α β
have _₁ : (@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: calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        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 : ℕ
t : (↑(Icc tmin tmax) : Type)
⊢ dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
have zero : ∀ (t : (↑(Icc tmin tmax) : Type)),
  dist (((next hf hx)^[0] α).toFun t) (((next hf hx)^[0] β).toFun t) ≤
    HPow.hPow (β := ℕ) ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) 0 / (↑0! : ℝ) * dist α β
Tactic: induction n generalizing t with
  | zero => simpa using
      ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _
  | succ n hn =>
    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)]
    calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        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]
Cleared hypotheses: n, 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 : ℕ
t : (↑(Icc tmin tmax) : Type)
zero :
  ∀ (t : (↑(Icc tmin tmax) : Type)),
    dist (((next hf hx)^[0] α).toFun t) (((next hf hx)^[0] β).toFun t) ≤
      HPow.hPow (β := ℕ) ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) 0 / (↑0! : ℝ) * dist α β
⊢ dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
have succ : ∀ (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 α β
Tactic: induction n generalizing t with
  | zero => simpa using
      ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _
  | succ n hn =>
    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)]
    calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        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]
Cleared hypotheses: n, 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 : ℕ
⊢ dist ((next hf hx)^[n] α) ((next hf hx)^[n] β) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
have rw : ∀ (x_1 : (↑(Icc tmin tmax) : Type)),
  dist (α := E)
      ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] α) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          x_1 :
        E)
      ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] β) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          x_1 :
        E) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
Tactic: rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq, ContinuousMap.dist_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 : ℕ
rw :
  ∀ (x_1 : (↑(Icc tmin tmax) : Type)),
    dist (α := E)
        ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] α) :
                C((↑(Icc tmin tmax) : Type), E)) :
              (a : (↑(Icc tmin tmax) : Type)) → E)
            x_1 :
          E)
        ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] β) :
                C((↑(Icc tmin tmax) : Type), E)) :
              (a : (↑(Icc tmin tmax) : Type)) → E)
            x_1 :
          E) ≤
      ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
⊢ dist ((next hf hx)^[n] α) ((next hf hx)^[n] β) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
have rw₁ : 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
Tactic: rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq, ContinuousMap.dist_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 : ℕ
t : (↑(Icc tmin tmax) : Type)
⊢ dist (α := E)
      ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] α) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          t :
        E)
      ((((toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) ((next hf hx)^[n] β) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          t :
        E) ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
have apply : ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β ≤
  ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
Tactic: apply le_trans <| dist_iterate_next_apply_le hf hx α β n 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 : ℕ
t : (↑(Icc tmin tmax) : Type)
⊢ ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
have hbc : |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
Tactic: gcongr
-- 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 : ℕ
⊢ 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
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
hf : IsPicardLindelof f t₀ x₀ a r L K
n : ℕ
hn : ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) < 1
⊢ 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ)
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