-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem exists_isPicardLindelof_const_of_contDiffAt (hv : ContDiffAt ℝ 1 v x₀) :
    ∃ ε > (0 : ℝ), ∃ L R C, IsPicardLindelof (fun _ => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L ((R₁ ⊓ R₂) / 2) (1 + ‖v x₀‖)

Tactic:
exact
  { ht₀ := Real.closedBall_eq_Icc ▸ mem_closedBall_self hε0.le
    hR := by positivity
    lipschitz := fun _ _ => hlip.mono <|
      (closedBall_subset_ball <| half_lt_self <| lt_min hR₁ hR₂).trans <|
      (Metric.ball_subset_ball <| min_le_left _ _).trans hball
    cont := fun _ _ => continuousOn_const
    norm_le := fun _ _ x hx => hbdd' x <| mem_of_mem_of_subset hx <|
      (closedBall_subset_ball <| half_lt_self <| lt_min hR₁ hR₂).trans <|
      (Metric.ball_subset_ball <| min_le_right _ _).trans (subset_refl _)
    C_mul_le_R := by
      rw [add_sub_cancel_left, sub_sub_cancel, max_self, hε, mul_div_left_comm, div_self, mul_one]
      exact ne_of_gt <| add_pos_of_pos_of_nonneg zero_lt_one <| norm_nonneg _ }

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ 0 ≤ (R₁ ⊓ R₂) / 2

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Tactic:
have hε0 : 0 < ε := hε ▸ div_pos (half_pos <| lt_min hR₁ hR₂)
  (add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _))

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Tactic:
have hbdd' : ∀ x ∈ Metric.ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖ := fun _ hx =>
  sub_le_iff_le_add.mp <| le_of_lt <| lt_of_abs_lt <| Real.dist_eq _ _ ▸ hbdd hx

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Tactic:
obtain ⟨L, s, hs, hlip⟩ := hv.exists_lipschitzOnWith

Result:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Proof state:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Tactic:
obtain ⟨R₁, hR₁ : 0 < R₁, hball⟩ := Metric.mem_nhds_iff.mp hs

Result:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
⊢ ∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ 1 + ‖v x₀‖ ≠ 0

Tactic:
exact ne_of_gt <| add_pos_of_pos_of_nonneg zero_lt_one <| norm_nonneg _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ (1 + ‖v x₀‖) * ((t₀ + ε - t₀) ⊔ (t₀ - (t₀ - ε))) ≤ (R₁ ⊓ R₂) / 2

Tactic:
rw [add_sub_cancel_left, sub_sub_cancel, max_self, hε, mul_div_left_comm, div_self, mul_one]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
hv : ContDiffAt ℝ 1 v x₀
L : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s
R₁ : ℝ
hR₁ : 0 < R₁
hball : ball x₀ R₁ ⊆ s
R₂ : ℝ
hR₂ : 0 < R₂
hbdd : ∀ ⦃x : E⦄, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1
hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖
ε : ℝ := (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε : ε = (R₁ ⊓ R₂) / 2 / (1 + ‖v x₀‖)
hε0 : 0 < ε
⊢ 1 + ‖v x₀‖ ≠ 0