awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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₀' : ℝ)
hbc₁ : (↑t₀' : ℝ) ≤ (↑t₀ : ℝ)
⊢ (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
linarith : (↑t₀' : ℝ) < (↑t₀ : ℝ) → (↑t₀ : ℝ) - (↑t₀' : ℝ) + ((↑t₀' : ℝ) - (↑t₀ : ℝ)) = 0
⊢ (↑t₀ : ℝ) ≤ (↑t₀' : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
linarith : (↑t₀ : ℝ) < (↑t₀' : ℝ) → -((↑t₀ : ℝ) - (↑t₀' : ℝ)) + ((↑t₀ : ℝ) - (↑t₀' : ℝ)) = 0
⊢ (↑t₀' : ℝ) ≤ (↑t₀ : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ℝ)

Tactic:
hf.mul_max_le

Premises used: IsPicardLindelof.mul_max_le
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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
calc : (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑L : ℝ) * max (tmax - (↑t₀ : ℝ)) ((↑t₀ : ℝ) - tmin)
⊢ (↑L : ℝ) * max (tmax' - (↑t₀' : ℝ)) ((↑t₀' : ℝ) - tmin') ≤ (↑a : ℝ) - (↑r : ℝ)

Tactic:
calc L * max (tmax' - t₀') (t₀' - tmin')
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) := by gcongr <;> linarith
    _ ≤ a - r := hf.mul_max_le

Premises used: HSub.hSub, Max.max, IsPicardLindelof.mul_max_le, Subtype.val
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f_1 : ℝ → E → E
tmin tmax : ℝ
t₀_1 : (↑(Icc tmin tmax) : Type)
x₀_1 x : E
a_1 r_1 L_1 K_1 : ℝ≥0
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
simp [le_of_lt hε]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f_1 : ℝ → E → E
tmin tmax : ℝ
t₀_1 : (↑(Icc tmin tmax) : Type)
x₀_1 x : E
a_1 r_1 L_1 K_1 : ℝ≥0
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 < ε'
⊢ t₀ ∈ Icc (t₀ - ε') (t₀ + ε')

Tactic:
simp [le_of_lt hε']

Premises used: le_of_lt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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'
⊢ 0 < (↑a' : ℝ) - (↑r' : ℝ)

Tactic:
simp only [sub_pos, NNReal.coe_lt_coe, hr]

Premises used: sub_pos, NNReal.coe_lt_coe
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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'
⊢ 0 < (↑a' : ℝ) - (↑r' : ℝ)

Tactic:
have ha'r' : (0 : ℝ) < a' - r' := by simp only [sub_pos, NNReal.coe_lt_coe, hr]
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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))
⊢ 0 < ((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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))
⊢ 0 < ε'

Tactic:
have hε'pos : 0 < ε' := lt_min hε (by positivity)
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 < ε'
⊢ ε' ≤ ε

Tactic:
have hε'_le : ε' ≤ ε := min_le_left _ _
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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₀ ∈ Icc (t₀ - ε') (t₀ + ε')

Tactic:
simp [le_of_lt hε'pos]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
linarith : t₀ - ε' < t₀ - ε → ε' - ε + (t₀ - ε' - (t₀ - ε)) = 0
⊢ t₀ - ε ≤ t₀ - ε'

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
linarith : t₀ + ε < t₀ + ε' → ε' - ε + (t₀ + ε - (t₀ + ε')) = 0
⊢ t₀ + ε' ≤ t₀ + ε

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
refine :
  (↑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' : ℝ)
⊢ ∃ (ε' : ℝ) (hε' : 0 < ε'),
    IsPicardLindelof f (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε') (t₀ + ε')) t₀ ⋯) x₀ a' r' L K

Tactic:
refine ⟨ε', hε'pos, hf.shrink ⟨t₀, by simp [le_of_lt hε'pos]⟩ (by linarith) (by linarith) ha ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
simp : (↑L : ℝ) * ε' ≤ (↑a' : ℝ) - (↑r' : ℝ)
⊢ (↑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' : ℝ)

Tactic:
simp only [add_sub_cancel_left, sub_sub_cancel, max_self]

Premises used: add_sub_cancel_left, max_self, sub_sub_cancel
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
hbc : ε' ≤ ((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)
⊢ (↑L : ℝ) * ε' ≤ (↑L : ℝ) * (((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1))

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
⊢ ε' ≤ ((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)

Tactic:
min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
⊢ ε' ≤ ((↑a' : ℝ) - (↑r' : ℝ)) / ((↑L : ℝ) + 1)

Tactic:
exact min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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' : ℝ)) / ((↑L : ℝ) + 1)) = (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
hbc : (↑L : ℝ) / ((↑L : ℝ) + 1) ≤ 1
⊢ (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ)) ≤ 1 * ((↑a' : ℝ) - (↑r' : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
⊢ 0 < (↑L : ℝ) + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
hbc : (↑L : ℝ) ≤ (↑L : ℝ) + 1
⊢ (↑L : ℝ) / ((↑L : ℝ) + 1) ≤ 1

Tactic:
rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]

Premises used: div_le_one
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
linarith : (↑L : ℝ) + 1 < (↑L : ℝ) → -1 + ((↑L : ℝ) + 1 - (↑L : ℝ)) = 0
⊢ (↑L : ℝ) ≤ (↑L : ℝ) + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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 : ε' ≤ ε
⊢ 1 * ((↑a' : ℝ) - (↑r' : ℝ)) = (↑a' : ℝ) - (↑r' : ℝ)

Tactic:
one_mul _

Premises used: one_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
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' : ℝ))
calc₂ : (↑L : ℝ) / ((↑L : ℝ) + 1) * ((↑a' : ℝ) - (↑r' : ℝ)) ≤ 1 * ((↑a' : ℝ) - (↑r' : ℝ))
⊢ (↑L : ℝ) * ε' ≤ (↑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 _

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, NNReal.toReal, one_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f_1 : ℝ → E → E
tmin tmax : ℝ
t₀_1 : (↑(Icc tmin tmax) : Type)
x₀_1 x : E
a_1 r_1 L_1 K_1 : ℝ≥0
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
ε : ℝ
hε : 0 < ε
a r L K : ℝ≥0
h : 0 < r
t₀ : ℝ
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)

Tactic:
simp [le_of_lt hε]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
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₀ ⋯) x₀ a r L K
⊢ ∃ (ε : ℝ) (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

Tactic:
obtain ⟨K, s, hs, hl⟩ := hf.exists_lipschitzOnWith

Premises used: ContDiffAt.exists_lipschitzOnWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
obtain :
  ∀ (a : ℝ) (ha : 0 < a) (has : ball x₀ a ⊆ 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₀ ⋯) x₀ a r L K
⊢ ∃ (ε : ℝ) (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

Tactic:
obtain ⟨a, ha : 0 < a, has⟩ := Metric.mem_nhds_iff.mp hs

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
⊢ let L := (↑K : ℝ) * a + ‖f x₀‖ + 1;
  L = (↑K : ℝ) * a + ‖f x₀‖ + 1

Tactic:
set L := K * a + ‖f x₀‖ + 1 with hL
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
⊢ 0 < L

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
⊢ 0 < L

Tactic:
have hL0 : 0 < L := by positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
rw : ‖f x‖ ≤ (↑K : ℝ) * a + ‖f x₀‖ + 1
⊢ ‖f x‖ ≤ L

Tactic:
rw [hL]
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ ‖f x‖ ≤ ‖f x - f x₀‖ + ‖f x₀‖

Tactic:
norm_le_norm_sub_add _ _

Premises used: norm_le_norm_sub_add
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
bc : ‖f x - f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖
⊢ ‖f x - f x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
apply : x ∈ s
⊢ ‖f x - f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖

Tactic:
apply hl.norm_sub_le _ (mem_of_mem_nhds hs)

Premises used: LipschitzOnWith.norm_sub_le, mem_of_mem_nhds
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
apply : closedBall x₀ (a / 2) ⊆ ball x₀ a
⊢ x ∈ s

Tactic:
apply subset_trans _ has hx

Premises used: subset_trans
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ closedBall x₀ (a / 2) ⊆ ball x₀ a

Tactic:
closedBall_subset_ball <| half_lt_self ha

Premises used: half_lt_self, Metric.closedBall_subset_ball
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ closedBall x₀ (a / 2) ⊆ ball x₀ a

Tactic:
exact closedBall_subset_ball <| half_lt_self ha

Premises used: half_lt_self, Metric.closedBall_subset_ball
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
bc : ‖x - x₀‖ ≤ a
⊢ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * a + ‖f x₀‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
bc : x ∈ closedBall x₀ a
⊢ ‖x - x₀‖ ≤ a

Tactic:
rw [← mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ x ∈ closedBall x₀ a

Tactic:
closedBall_subset_closedBall (half_le_self (le_of_lt ha)) hx

Premises used: le_of_lt, half_le_self, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ x ∈ closedBall x₀ a

Tactic:
exact closedBall_subset_closedBall (half_le_self (le_of_lt ha)) hx

Premises used: le_of_lt, half_le_self, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ (↑K : ℝ) * a + ‖f x₀‖ ≤ L

Tactic:
le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right