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
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
⊢ t₀ ≤ tmax
have linarith : tmax < t₀ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : tmax < t₀ → 2 / 2 = 1
⊢ t₀ ≤ tmax
have linarith₁ : tmax < t₀ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : tmax < t₀ → 2 / 2 = 1
linarith₁ : tmax < t₀ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ t₀ ≤ tmax
have linarith₂ : tmax < t₀ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
linarith : tmax < t₀ → 2 / 2 = 1
linarith₁ : tmax < t₀ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : tmax < t₀ → GT.gt (α := ℝ) 2 0
⊢ t₀ ≤ tmax
have linarith₃ : tmax < t₀ → tmin - tmax + (2 * t₀ - (1 * tmin + 1 * tmax)) + 2 * (tmax - t₀) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have ht₀ : t₀ ∈ Icc tmin tmax
Tactic: have ht₀ : t₀ ∈ Icc tmin tmax := ⟨by linarith, by linarith⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
ht₀ : t₀ ∈ Icc tmin tmax
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ α t = picard f t₀ (α t₀) α t
have this : uIcc t₀ t ⊆ Icc tmin tmax
Tactic: have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
ht₀ : t₀ ∈ Icc tmin tmax
t : ℝ
ht : t ∈ Icc tmin tmax
this : uIcc t₀ t ⊆ Icc tmin tmax
⊢ α t = picard f t₀ (α t₀) α t
have rw : α t = α t
Tactic: rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmin < tmax
t₀ : ℝ := (tmin + tmax) / 2
h : t₀ = (tmin + tmax) / 2
ht₀ : t₀ ∈ Icc tmin tmax
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have this : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t
Tactic: have : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ (α t₀) α t := by
      intro t ht
      have : uIcc t₀ t ⊆ Icc tmin tmax := uIcc_subset_Icc ht₀ ht
      rw [picard_eq_of_hasDerivAt (hf.continuousOn.mono (prod_subset_prod_left this))
        (fun t' ht' ↦ hα t' (this ht') |>.mono this) (hmem.mono_left this)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : ¬tmin < tmax
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have hlt₁ : tmax < tmin ∨ tmax = tmin
Tactic: rw [not_lt, le_iff_lt_or_eq] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
x : ℝ
ht : x ∈ Icc tmin tmax
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax) x
have ht₁ : Membership.mem (γ := Set ℝ) ∅ x
Tactic: rw [Icc_eq_empty (not_le.mpr h)] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) ∅ x
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax) x
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax = tmin
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have neg : ContDiffOn ℝ (↑n : WithTop ℕ∞) α {tmin}
Tactic: rw [h, Icc_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax = tmin
x : ℝ
ht : Membership.mem (γ := Set ℝ) {tmin} x
⊢ ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} x
have neg : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) α {tmin} tmin
Tactic: rw [eq_of_mem_singleton ht]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmax < tmin ∨ tmax = tmin
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have neg : ∀ (h : tmax < tmin), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
Tactic: cases hlt with
    | inl h =>
      intro _ ht
      rw [Icc_eq_empty (not_le.mpr h)] at ht
      exfalso
      exact notMem_empty _ ht
    | inr h =>
      rw [h, Icc_self]
      intro _ ht
      rw [eq_of_mem_singleton ht]
      exact contDiffWithinAt_singleton
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
hlt : tmax < tmin ∨ tmax = tmin
neg : ∀ (h : tmax < tmin), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
have neg₁ : ∀ (h : tmax = tmin), ContDiffOn ℝ (↑n : WithTop ℕ∞) α (Icc tmin tmax)
Tactic: cases hlt with
    | inl h =>
      intro _ ht
      rw [Icc_eq_empty (not_le.mpr h)] at ht
      exfalso
      exact notMem_empty _ ht
    | inr h =>
      rw [h, Icc_self]
      intro _ ht
      rw [eq_of_mem_singleton ht]
      exact contDiffWithinAt_singleton
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ IsPicardLindelof f t₀' x₀ a r L K
have apply : (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑a : ℝ) - (↑r : ℝ)
Tactic: apply hf.shrink t₀' htmin htmax le_rfl
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
have hbc : (↑t₀ : ℝ) ≤ (↑t₀' : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
hbc : (↑t₀ : ℝ) ≤ (↑t₀' : ℝ)
⊢ (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
have hbc₁ : (↑t₀' : ℝ) ≤ (↑t₀ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ (↑t₀ : ℝ) ≤ (↑t₀' : ℝ)
have linarith : (↑t₀' : ℝ) < (↑t₀ : ℝ) → (↑t₀ : ℝ) - (↑t₀' : ℝ) + ((↑t₀' : ℝ) - (↑t₀ : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ (↑t₀' : ℝ) ≤ (↑t₀ : ℝ)
have linarith : (↑t₀ : ℝ) < (↑t₀' : ℝ) → -((↑t₀ : ℝ) - (↑t₀' : ℝ)) + ((↑t₀ : ℝ) - (↑t₀' : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : (↑(Icc tmin' tmax') : Type)
ht₀ : (↑t₀ : ℝ) = (↑t₀' : ℝ)
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑a : ℝ) - (↑r : ℝ)
have calc : (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
Tactic: calc L * max (tmax' - t₀') (t₀' - tmin')
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) := by gcongr <;> linarith
    _ ≤ a - r := hf.mul_max_le
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
⊢ ∃ (ε' : ℝ) (hε' : 0 < ε'),
    IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) x₀ a' r' L K
have ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
Tactic: have ha'r' : (0 : ℝ) < a' - r' := by simp only [sub_pos, NNReal.coe_lt_coe, hr]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
⊢ ∃ (ε' : ℝ) (hε' : 0 < ε'),
    IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) x₀ a' r' L K
have hε'pos : 0 < ε'
Tactic: have hε'pos : 0 < ε' := lt_min hε (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
⊢ ∃ (ε' : ℝ) (hε' : 0 < ε'),
    IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) x₀ a' r' L K
have hε'_le : ε' ≤ ε
Tactic: have hε'_le : ε' ≤ ε := min_le_left _ _
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ t₀ - ε ≤ t₀ - ε'
have linarith : t₀ - ε' < t₀ - ε → ε' - ε + (t₀ - ε' - (t₀ - ε)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ t₀ + ε' ≤ t₀ + ε
have linarith : t₀ + ε < t₀ + ε' → ε' - ε + (t₀ + ε - (t₀ + ε')) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ ∃ (ε' : ℝ) (hε' : 0 < ε'),
    IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) x₀ a' r' L K
have refine : (↑L : ℝ) *
    max (t₀ + ε' - (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ sorry) : ℝ))
      ((↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ sorry) : ℝ) - (t₀ - ε')) ≤
  (↑a' : ℝ) - (↑r' : ℝ)
Tactic: refine ⟨ε', hε'pos, hf.shrink ⟨t₀, by simp [le_of_lt hε'pos]⟩ (by linarith) (by linarith) ha ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) *
      max (t₀ + ε' - (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) : ℝ))
        ((↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) : ℝ) - (t₀ - ε')) ≤
    (↑a' : ℝ) - (↑r' : ℝ)
have simp : (↑L : ℝ) * ε' ≤ (↑a' : ℝ) - (↑r' : ℝ)
Tactic: simp only [add_sub_cancel_left, sub_sub_cancel, max_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) * ε' ≤ (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
have hbc : ε' ≤ ((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ)) ≤ 1 * ((↑a' : ℝ) - (↑r' : ℝ))
have hbc : (↑L : ℝ) / ((↑L : ℝ) + 1) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) / ((↑L : ℝ) + 1) ≤ 1
have hbc : (↑L : ℝ) ≤ (↑L : ℝ) + 1
Tactic: rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) ≤ (↑L : ℝ) + 1
have linarith : (↑L : ℝ) + 1 < (↑L : ℝ) → -1 + ((↑L : ℝ) + 1 - (↑L : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ (↑L : ℝ) * ε' ≤ (↑a' : ℝ) - (↑r' : ℝ)
have calc : (↑L : ℝ) * ε' ≤ (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
Tactic: calc (L : ℝ) * ε'
    _ ≤ L * ((a' - r') / (L + 1)) := by gcongr; exact min_le_right _ _
    _ = L / (L + 1) * (a' - r') := by ring
    _ ≤ 1 * (a' - r') := by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith
    _ = a' - r' := one_mul _
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
calc : (↑L : ℝ) * ε' ≤ (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
⊢ (↑L : ℝ) * ε' ≤ (↑a' : ℝ) - (↑r' : ℝ)
have calc₁ : (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)) = (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ))
Tactic: calc (L : ℝ) * ε'
    _ ≤ L * ((a' - r') / (L + 1)) := by gcongr; exact min_le_right _ _
    _ = L / (L + 1) * (a' - r') := by ring
    _ ≤ 1 * (a' - r') := by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith
    _ = a' - r' := one_mul _
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < (↑a' : ℝ) - (↑r' : ℝ)
ε' : ℝ := min ε (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
calc : (↑L : ℝ) * ε' ≤ (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))
calc₁ : (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)) = (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ))
⊢ (↑L : ℝ) * ε' ≤ (↑a' : ℝ) - (↑r' : ℝ)
have calc₂ : (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ)) ≤ 1 * ((↑a' : ℝ) - (↑r' : ℝ))
Tactic: calc (L : ℝ) * ε'
    _ ≤ L * ((a' - r') / (L + 1)) := by gcongr; exact min_le_right _ _
    _ = L / (L + 1) * (a' - r') := by ring
    _ ≤ 1 * (a' - r') := by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith
    _ = a' - r' := one_mul _
-- 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
⊢ ∃ (ε : ℝ) (hε : 0 < ε) (a : ℝ≥0) (r : ℝ≥0) (L : ℝ≥0) (K : ℝ≥0) (_ : 0 < r),
    ∀ (t₀ : ℝ),
      IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K
have obtain : ∀ (K : ℝ≥0) (s : Set E) (hs : s ∈ 𝓝 x₀) (hl : LipschitzOnWith K f s),
  ∃ (ε : ℝ) (hε : 0 < ε) (a : ℝ≥0) (r : ℝ≥0) (L : ℝ≥0) (K : ℝ≥0) (_ : 0 < r),
    ∀ (t₀ : ℝ),
      IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ sorry) x₀ a r L K
Tactic: obtain ⟨K, s, hs, hl⟩ := hf.exists_lipschitzOnWith