awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
t : ℝ
ht : t ∈ Icc tmin tmax
rw : α.toFun (projIcc tmin tmax ⋯ t) = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
rw₁ :
  α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht) =
    α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
hx : t ∈ Icc tmin tmax
rw₂ :
  α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht) =
    α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)
hx₁ : t ∈ Icc tmin tmax
⊢ α.compProj t = α.toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht)

Tactic:
rw [compProj_apply, projIcc_of_mem]

Premises used: Set.projIcc_of_mem, ODE.FunSpace.compProj_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
r L : ℝ≥0
α : FunSpace t₀ x₀ r L
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] α.compProj

Tactic:
α.continuous.comp continuous_projIcc

Premises used: Continuous.comp, ODE.FunSpace.compProj, continuous_projIcc, ODE.FunSpace.continuous
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
rw : ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)
⊢ α.toFun t ∈ closedBall x₀ (↑a : ℝ)

Tactic:
rw [mem_closedBall, dist_eq_norm]

Premises used: dist_eq_norm, Metric.mem_closedBall
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ ‖α.toFun t - x₀‖ ≤ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖

Tactic:
norm_sub_le_norm_sub_add_norm_sub ..

Premises used: norm_sub_le_norm_sub_add_norm_sub
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
apply : ‖α.toFun t - α.toFun t₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|
⊢ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)

Tactic:
apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀

Premises used: add_le_add, mem_closedBall_iff_norm, Iff.mp, ODE.FunSpace.mem_closedBall₀
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
rw : dist (α.toFun t) (α.toFun t₀) ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|
⊢ ‖α.toFun t - α.toFun t₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|

Tactic:
rw [← dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ dist (α.toFun t) (α.toFun t₀) ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|

Tactic:
α.lipschitzWith.dist_le_mul t t₀

Premises used: LipschitzWith.dist_le_mul, ODE.FunSpace.lipschitzWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ dist (α.toFun t) (α.toFun t₀) ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|

Tactic:
exact α.lipschitzWith.dist_le_mul t t₀

Premises used: LipschitzWith.dist_le_mul, ODE.FunSpace.lipschitzWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
bc : |(↑t : ℝ) - (↑t₀ : ℝ)| ≤ max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ) ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
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
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
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
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ) ≤ (↑a : ℝ) - (↑r : ℝ) + (↑r : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
⊢ (↑a : ℝ) - (↑r : ℝ) + (↑r : ℝ) = (↑a : ℝ)

Tactic:
sub_add_cancel _ _

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : (↑(Icc tmin tmax) : Type)
t₁ : ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ)
t₂ : (↑L : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)| + (↑r : ℝ) ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ)
t₃ : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) + (↑r : ℝ) ≤ (↑a : ℝ) - (↑r : ℝ) + (↑r : ℝ)
⊢ ‖α.toFun t - x₀‖ ≤ (↑a : ℝ)

Tactic:
calc
    ‖α t - x₀‖ ≤ ‖α t - α t₀‖ + ‖α t₀ - x₀‖ := norm_sub_le_norm_sub_add_norm_sub ..
    _ ≤ L * |t.1 - t₀.1| + r := by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) + r := by
      gcongr
      exact abs_sub_le_max_sub t.2.1 t.2.2 _
    _ ≤ a - r + r := by gcongr
    _ = a := sub_add_cancel _ _

Premises used: HSub.hSub, Max.max, ODE.FunSpace.toFun, Subtype.val, sub_add_cancel, norm_sub_le_norm_sub_add_norm_sub
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin) ≤ (↑a : ℝ) - (↑r : ℝ)
t : ℝ
⊢ α.compProj t ∈ closedBall x₀ (↑a : ℝ)

Tactic:
α.mem_closedBall h

Premises used: Set.Mem, ODE.FunSpace.compProj, ODE.FunSpace.mem_closedBall
-- 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
α : FunSpace t₀ x₀ r L
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) (Icc tmin tmax)

Tactic:
continuousOn_comp
    (continuousOn_prod_of_continuousOn_lipschitzOnWith' (uncurry f) K hf.lipschitzOnWith
      hf.continuousOn)
    α.continuous_compProj.continuousOn
    fun _ _ ↦ α.mem_closedBall hf.mul_max_le

Premises used: Continuous.continuousOn, IsPicardLindelof.continuousOn, IsPicardLindelof.lipschitzOnWith, ODE.FunSpace.mem_closedBall, continuousOn_prod_of_continuousOn_lipschitzOnWith', ODE.FunSpace.continuous_compProj, IsPicardLindelof.mul_max_le, Function.uncurry, ODE.continuousOn_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
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
hu : ContinuousOn.{0, u_1} (Y := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) (uIcc (↑t₀ : ℝ) (↑t : ℝ))
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) volume (↑t₀ : ℝ) (↑t : ℝ)

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- 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
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
hu : uIcc (↑t₀ : ℝ) (↑t : ℝ) ⊆ Icc tmin tmax
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (t' : ℝ) ↦ f t' (α.compProj t')) (uIcc (↑t₀ : ℝ) (↑t : ℝ))

Tactic:
apply α.continuousOn_comp_compProj hf |>.mono

Premises used: ODE.FunSpace.continuousOn_comp_compProj, ContinuousOn.mono
-- 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
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
⊢ uIcc (↑t₀ : ℝ) (↑t : ℝ) ⊆ Icc tmin tmax

Tactic:
uIcc_subset_Icc t₀.2 t.2

Premises used: Set.uIcc_subset_Icc, 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₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : FunSpace t₀ x₀ r L
t : (↑(Icc tmin tmax) : Type)
⊢ uIcc (↑t₀ : ℝ) (↑t : ℝ) ⊆ Icc tmin tmax

Tactic:
exact uIcc_subset_Icc t₀.2 t.2

Premises used: Set.uIcc_subset_Icc, 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 y : 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
t₁ t₂ : (↑(Icc tmin tmax) : Type)
rw : norm.{u_1} (E := E) (∫ (x : ℝ) in (↑t₂ : ℝ)..(↑t₁ : ℝ), f x (α.compProj x)) ≤ (↑L : ℝ) * |(↑t₁ : ℝ) - (↑t₂ : ℝ)|
⊢ dist (picard f (↑t₀ : ℝ) x α.compProj (↑t₁ : ℝ)) (picard f (↑t₀ : ℝ) x α.compProj (↑t₂ : ℝ)) ≤ (↑L : ℝ) * dist t₁ t₂

Tactic:
rw [dist_eq_norm, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      integral_interval_sub_left (intervalIntegrable_comp_compProj hf _ t₁)
        (intervalIntegrable_comp_compProj hf _ t₂), Subtype.dist_eq, Real.dist_eq]

Premises used: dist_eq_norm, add_sub_add_left_eq_sub, Subtype.dist_eq, Real.dist_eq, ODE.FunSpace.intervalIntegrable_comp_compProj, intervalIntegral.integral_interval_sub_left, 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 y : 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
t₁ t₂ : (↑(Icc tmin tmax) : Type)
h : ∀ x ∈ uIoc (↑t₂ : ℝ) (↑t₁ : ℝ), ‖f x (α.compProj x)‖ ≤ (↑L : ℝ)
⊢ norm.{u_1} (E := E) (∫ (x : ℝ) in (↑t₂ : ℝ)..(↑t₁ : ℝ), f x (α.compProj x)) ≤ (↑L : ℝ) * |(↑t₁ : ℝ) - (↑t₂ : ℝ)|

Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le_const

Premises used: intervalIntegral.norm_integral_le_of_norm_le_const
-- 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 : ℝ)
α : FunSpace t₀ x₀ r L
t₁ t₂ : (↑(Icc tmin tmax) : Type)
t : ℝ
ht : t ∈ uIoc (↑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 y : 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
t₁ t₂ : (↑(Icc tmin tmax) : Type)
t : ℝ
ht_1 : t ∈ uIoc (↑t₂ : ℝ) (↑t₁ : ℝ)
ht : t ∈ Icc tmin tmax
⊢ ‖f t (α.compProj t)‖ ≤ (↑L : ℝ)

Tactic:
hf.norm_le _ ht _ <| α.mem_closedBall hf.mul_max_le

Premises used: IsPicardLindelof.norm_le, ODE.FunSpace.mem_closedBall, IsPicardLindelof.mul_max_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 y : 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
t₁ t₂ : (↑(Icc tmin tmax) : Type)
t : ℝ
ht_1 : t ∈ uIoc (↑t₂ : ℝ) (↑t₁ : ℝ)
ht : t ∈ Icc tmin tmax
⊢ ‖f t (α.compProj t)‖ ≤ (↑L : ℝ)

Tactic:
exact hf.norm_le _ ht _ <| α.mem_closedBall hf.mul_max_le

Premises used: IsPicardLindelof.norm_le, ODE.FunSpace.mem_closedBall, IsPicardLindelof.mul_max_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 y : 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
⊢ picard f (↑t₀ : ℝ) x α.compProj (↑t₀ : ℝ) ∈ closedBall x₀ (↑r : ℝ)

Tactic:
simp [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₀ 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
t : (↑(Icc tmin tmax) : Type)
⊢ (next hf hx α).toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)

Tactic:
rfl

Premises used: ODE.picard, rfl
-- 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
⊢ (next hf hx α).toFun t₀ = x

Tactic:
simp
-- 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
mp : IsFixedPt (next hf hx) α → ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
mpr :
  (∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)) → IsFixedPt (next hf hx) α
⊢ IsFixedPt (next hf hx) α ↔ ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)

Tactic:
constructor
-- 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
⊢ IsFixedPt (next hf hx) α → ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)

Tactic:
fun hα t ↦ congrArg (· t) hα |>.symm
-- 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
⊢ IsFixedPt (next hf hx) α → ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)

Tactic:
exact fun hα t ↦ congrArg (· t) hα |>.symm

Premises used: congrArg, Eq.symm
-- 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
h : ∀ (t : (↑(Icc tmin tmax) : Type)), α.toFun t = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
mpr : ∀ (t : (↑(Icc tmin tmax) : Type)), (next hf hx α).toFun t = α.toFun t
⊢ IsFixedPt (next hf hx) α

Tactic:
ext t
-- 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
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 : ℝ)
mpr₁ mpr₂ : picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ) = picard f (↑t₀ : ℝ) x α.compProj (↑t : ℝ)
⊢ (next hf hx α).toFun t = α.toFun t

Tactic:
rw [h, next_apply]

Premises used: ODE.FunSpace.next_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 : ℝ)
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 α β
rw :
  (↑K : ℝ) * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    (↑K : ℝ) * ((↑K : ℝ) ^ n * |(↑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 α β

Tactic:
rw [pow_succ', mul_assoc, mul_div_assoc, mul_assoc]

Premises used: mul_assoc, mul_div_assoc, pow_succ'
-- 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 : ℝ)
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 α β
hbc :
  dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    (↑K : ℝ) ^ n * |(↑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 α β)

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 : ℝ)
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 α β
hbc hbc₁ hbc₂ hbc₃ :
  dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ((↑K : ℝ) * |(↑t : ℝ) - (↑t₀ : ℝ)|) ^ n / (↑n ! : ℝ) * dist α β
⊢ dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    (↑K : ℝ) ^ n * |(↑t : ℝ) - (↑t₀ : ℝ)| ^ n / (↑n ! : ℝ) * dist α β

Tactic:
rwa [← mul_pow]

Premises used: mul_pow
-- 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
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:
simpa using
      ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _

Premises used: ContinuousMap.dist_apply_le_dist
-- 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)
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 α β
⊢ dist (((next hf hx)^[n + 1] α).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    ((↑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)]

Premises used: Function.iterate_succ_apply', ODE.FunSpace.next_apply, dist_eq_norm, add_sub_add_left_eq_sub, intervalIntegral.integral_sub, ODE.FunSpace.intervalIntegrable_comp_compProj, 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 : ℕ
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)
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 α β
⊢ 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:
rw [intervalIntegral.norm_intervalIntegral_eq]

Premises used: intervalIntegral.norm_intervalIntegral_eq