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 : 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)
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ (↑K : ℝ) ^ (n + 1) * |x - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β

Tactic:
fun_prop
-- 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 : ℕ
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)
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 α β
⊢ 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:
apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))

Premises used: MeasureTheory.norm_integral_le_of_norm_le, Continuous.integrableOn_uIoc
-- 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 : ℕ
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)
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 α β
⊢ ∀ᵐ (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 ae_restrict_mem measurableSet_Ioc |>.mono

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono, measurableSet_Ioc
-- 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 : ℕ
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 : ℝ))
⊢ t' ∈ Icc tmin tmax

Tactic:
have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
-- 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 : ℕ
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
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 α β
rw₁ rw₂ : 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 α β

Tactic:
rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]

Premises used: dist_eq_norm, ODE.FunSpace.compProj_of_mem
-- 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 : ℕ
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
⊢ 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:
dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)

Premises used: ODE.FunSpace.dist_comp_iterate_next_le, Subtype.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₀ 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 :
  |@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 α β
⊢ (@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

Premises used: le_of_abs_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 : ℕ
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 α β
_₁ :
  (@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 α β
⊢ 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:
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]

Premises used: HMul.hMul, abs, Set.uIoc, HSub.hSub, HAdd.hAdd, Dist.dist, OfNat.ofNat, Subtype.val, 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
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 α β
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 α β
⊢ dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * 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]

Premises used: Function.iterate_succ_apply', ODE.FunSpace.next_apply, dist_eq_norm, HMul.hMul, abs, ContinuousMap.dist_apply_le_dist, add_sub_add_left_eq_sub, Set.uIoc, HSub.hSub, intervalIntegral.integral_sub, HAdd.hAdd, ODE.FunSpace.intervalIntegrable_comp_compProj, Dist.dist, OfNat.ofNat, Subtype.val, NNReal.toReal, ODE.picard_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 :
  ∀ (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 α β
rw₁ : 0 ≤ ((↑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 α β

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

Premises used: ODE.FunSpace.toContinuousMap, ContinuousMap.dist_le, 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 : 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)
apply :
  ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β
⊢ 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 α β

Tactic:
apply le_trans <| dist_iterate_next_apply_le hf hx α β n t

Premises used: ODE.FunSpace.dist_iterate_next_apply_le, 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
n : ℕ
t : (↑(Icc tmin tmax) : Type)
hbc : |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β ≤
    ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β

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
n : ℕ
t : (↑(Icc tmin tmax) : Type)
⊢ |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)

Tactic:
abs_sub_le_max_sub t.2.1 t.2.2 _

Premises used: And.right, And.left, abs_sub_le_max_sub, Subtype.property
-- 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 : ℕ
t : (↑(Icc tmin tmax) : Type)
⊢ |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)

Tactic:
exact abs_sub_le_max_sub t.2.1 t.2.2 _

Premises used: And.right, And.left, abs_sub_le_max_sub, Subtype.property
-- 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 : ℕ
⊢ 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₀ 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 : ℕ
this : 0 ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) * dist α β

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
hf : IsPicardLindelof f t₀ x₀ a r L K
n : ℕ
hn : ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) < 1
⊢ 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
hf : IsPicardLindelof f t₀ x₀ a r L K
n : ℕ
hn : ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ) < 1
this : 0 ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ 0 ≤ ((↑K : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)) ^ n / (↑n ! : ℝ)

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
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 ! : ℝ)

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
-- 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
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]

Tactic:
⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩

Premises used: Subtype.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
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 ! : ℝ)
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]
⊢ ∃ (n : ℕ) (C : ℝ≥0), ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ContractingWith C (next hf hx)^[n]

Tactic:
refine ⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩
-- 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
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 ! : ℝ)
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:
⟨hn, LipschitzWith.of_dist_le_mul fun α β ↦ dist_iterate_next_iterate_next_le hf hx α β n⟩

Premises used: ODE.FunSpace.dist_iterate_next_iterate_next_le, And.intro, ContractingWith, LipschitzWith.of_dist_le_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₀ : 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 ! : ℝ)
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:
exact ⟨hn, LipschitzWith.of_dist_le_mul fun α β ↦ dist_iterate_next_iterate_next_le hf hx α β n⟩
-- 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
inst_2 : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
⊢ ∃ (α : FunSpace t₀ x₀ r L), IsFixedPt (next hf hx) α

Tactic:
let ⟨_, _, h⟩ := exists_contractingWith_iterate_next hf
  ⟨_, h x hx |>.isFixedPt_fixedPoint_iterate⟩

Premises used: ODE.FunSpace.exists_contractingWith_iterate_next, Exists, Nat.iterate, ODE.FunSpace.next, ContractingWith.fixedPoint, Exists.intro, Function.IsFixedPt, ContractingWith.isFixedPt_fixedPoint_iterate, _private.0.ODE.FunSpace.exists_isFixedPt_next.match_1
-- 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
⊢ Nonempty (↑(Icc tmin tmax) : Type)

Tactic:
have : Nonempty (Icc tmin tmax) := ⟨t₀⟩