-- Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean
/-- If there exists `ε > 0` such that the local integral curve at each point `x : M` is defined at
least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve
passing through it.

See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/
lemma exists_isIntegralCurve_of_isIntegralCurveOn [BoundarylessManifold I M]
    {v : (x : M) → TangentSpace I x}
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
    {ε : ℝ} (hε : 0 < ε) (h : ∀ x : M, ∃ γ : ℝ → M, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε))
    (x : M) : ∃ γ : ℝ → M, γ 0 = x ∧ IsIntegralCurve γ v

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x => x + (asup - ε / 2)
hγ1 : IsIntegralCurveOn γ1 v (Ioo (ε / 2 - asup - ε) (ε / 2 - asup + ε))
γ1_def : γ1 = γ1_aux ∘ fun x => x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x => x - (asup - ε / 2)
hγ2 : IsIntegralCurveOn γ2 v (Ioo (asup - ε / 2 - ε) (asup - ε / 2 + ε))
γ2_def : γ2 = γ2_aux ∘ fun x => x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ 0 < a

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x => x + (asup - ε / 2)
hγ1 : IsIntegralCurveOn γ1 v (Ioo (ε / 2 - asup - ε) (ε / 2 - asup + ε))
γ1_def : γ1 = γ1_aux ∘ fun x => x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x => x - (asup - ε / 2)
hγ2 : IsIntegralCurveOn γ2 v (Ioo (asup - ε / 2 - ε) (asup - ε / 2 + ε))
γ2_def : γ2 = γ2_aux ∘ fun x => x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ (Ioo (-a) a).piecewise γ γ1 (asup - ε / 2) = γ2 (asup - ε / 2)

Tactic:
rw [piecewise, if_pos ⟨by linarith, hlt⟩, ← heq2]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x => x + (asup - ε / 2)
hγ1 : IsIntegralCurveOn γ1 v (Ioo (ε / 2 - asup - ε) (ε / 2 - asup + ε))
γ1_def : γ1 = γ1_aux ∘ fun x => x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x => x - (asup - ε / 2)
hγ2 : IsIntegralCurveOn γ2 v (Ioo (asup - ε / 2 - ε) (asup - ε / 2 + ε))
γ2_def : γ2 = γ2_aux ∘ fun x => x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ IsIntegralCurveOn ((Ioo (-a) a).piecewise γ γ1) v (Ioo (-(asup + ε / 2)) a)

Tactic:
exact (isIntegralCurveOn_piecewise (t₀ := -(asup - ε / 2)) hv hγ hγ1
    ⟨⟨neg_lt_neg hlt, by linarith⟩, ⟨by linarith, by linarith⟩⟩ heq1.symm).mono
  (union_comm _ _ ▸ Ioo_subset_Ioo_union_Ioo (by linarith) (by linarith) le_rfl)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ¬BddAbove s
⊢ ∃ γ, γ 0 = x ∧ IsIntegralCurve γ v

Tactic:
rw [not_bddAbove_iff] at hbdd

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
⊢ ∃ γ, γ 0 = x ∧ IsIntegralCurve γ v

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
⊢ ∃ γ, γ 0 = x ∧ IsIntegralCurve γ v

Tactic:
let s := { a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a) }

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsIntegralCurveOn γ v (Ioo (-a) a)}
⊢ ∃ γ, γ 0 = x ∧ IsIntegralCurve γ v