case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 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
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
obtain ⟨L, s', hs', hlip⟩ :=
  ContDiffAt.exists_lipschitzOnWith ((hv.contDiffWithinAt (mem_of_mem_nhds hs)).contDiffAt hs)
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 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
obtain ⟨r, hr : 0 < r, hball⟩ := Metric.mem_nhds_iff.mp (inter_sets (𝓝 x₀) hs hs')
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
have hr' := (half_pos hr).le
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
obtain ⟨C, hC⟩ := (isCompact_closedBall x₀ (r / 2)).bddAbove_image <| hv.continuousOn.norm.mono
  (subset_inter_iff.mp ((closedBall_subset_ball (half_lt_self hr)).trans hball)).left
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
have hC' : 0 ≤ C := by
  apply (norm_nonneg (v x₀)).trans
  apply hC
  exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
set ε := if C = 0 then 1 else r / 2 / C with hε
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L (r / 2) C
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ ∃ ε, ε > 0 ∧ ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
refine' ⟨ε, hε0, L, r / 2, C, _⟩
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ≤ C
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ 0 ≤ C
apply (norm_nonneg (v x₀)).trans
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ∈ (fun x => ‖v x‖) '' closedBall x₀ (r / 2)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ≤ C
apply hC
no goals
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
⊢ ‖v x₀‖ ∈ (fun x => ‖v x‖) '' closedBall x₀ (r / 2)
exact ⟨x₀, ⟨mem_closedBall_self hr', rfl⟩⟩
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < if C = 0 then 1 else r / 2 / C
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < ε
rw [hε]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : C = 0
⊢ 0 < 1

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : ¬C = 0
⊢ 0 < r / 2 / C
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
⊢ 0 < if C = 0 then 1 else r / 2 / C
split_ifs with h
no goals
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : C = 0
⊢ 0 < 1
exact zero_lt_one
no goals
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
h : ¬C = 0
⊢ 0 < r / 2 / C
exact div_pos (half_pos hr) (lt_of_le_of_ne hC' (Ne.symm h))
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ closedBall t₀ ε
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ Icc (t₀ - ε) (t₀ + ε)
rw [← Real.closedBall_eq_Icc]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ t₀ ∈ closedBall t₀ ε
exact mem_closedBall_self hε0.le
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ (if C = 0 then C else C * (r / 2 / C)) ≤ r / 2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ C * max (t₀ + ε - t₀) (t₀ - (t₀ - ε)) ≤ r / 2
rw [add_sub_cancel', sub_sub_cancel, max_self, mul_ite, mul_one]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : C = 0
⊢ C ≤ r / 2

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : ¬C = 0
⊢ C * (r / 2 / C) ≤ r / 2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
⊢ (if C = 0 then C else C * (r / 2 / C)) ≤ r / 2
split_ifs with h
no goals
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : C = 0
⊢ C ≤ r / 2
rwa [← h] at hr'
no goals
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ProperSpace E
v : E → E
t₀ : ℝ
x₀ : E
s : Set E
hv : ContDiffOn ℝ 1 v s
hs : s ∈ 𝓝 x₀
L : ℝ≥0
s' : Set E
hs' : s' ∈ 𝓝 x₀
hlip : LipschitzOnWith L v s'
r : ℝ
hr : 0 < r
hball : ball x₀ r ⊆ s ∩ s'
hr' : 0 ≤ r / 2
C : ℝ
hC : C ∈ upperBounds ((fun x => ‖v x‖) '' closedBall x₀ (r / 2))
hC' : 0 ≤ C
ε : ℝ := if C = 0 then 1 else r / 2 / C
hε : ε = if C = 0 then 1 else r / 2 / C
hε0 : 0 < ε
h : ¬C = 0
⊢ C * (r / 2 / C) ≤ r / 2
exact (mul_div_cancel' (r / 2) h).le