-- 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 α β
h₈ :
  |(↑K : ℝ) ^ (n + 1)| * ||(↑t : ℝ) - (↑t₀ : ℝ)| ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| / |(↑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]