-- Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean
/-- The extension of an integral curve by another integral curve is an integral curve.

If two integral curves are defined on overlapping open intervals, and they agree at a point in
their common domain, then they can be patched together to form a longer integral curve.

This is stated for manifolds without boundary for simplicity. We actually only need to assume that
the images of `γ` and `γ'` lie in the interior of the manifold.
TODO: Generalise to manifolds with boundary. -/
lemma isIntegralCurveOn_piecewise [BoundarylessManifold I M]
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
    {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Ioo a b))
    (hγ' : IsIntegralCurveOn γ' v (Ioo a' b')) {t₀ : ℝ}
    (ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b') (h : γ t₀ = γ' t₀) :
    IsIntegralCurveOn (piecewise (Ioo a b) γ γ') v (Ioo a b ∪ Ioo a' b')

Proof state:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ (Ioo a b).piecewise γ γ' =ᶠ[𝓝 t] γ

Tactic:
rw [Filter.eventuallyEq_iff_exists_mem]

Result:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ ∃ s ∈ 𝓝 t, EqOn ((Ioo a b).piecewise γ γ') γ s

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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
⊢ IsIntegralCurveOn ((Ioo a b).piecewise γ γ') v (Ioo a b ∪ Ioo a' b')

Tactic:
intros t ht

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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I ((Ioo a b).piecewise γ γ') t
    (ContinuousLinearMap.smulRight 1 (v ((Ioo a b).piecewise γ γ' t)))

Proof state:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I ((Ioo a b).piecewise γ γ') t
    (ContinuousLinearMap.smulRight 1 (v ((Ioo a b).piecewise γ γ' t)))

Tactic:
rw [piecewise, if_pos hmem]

Result:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I ((Ioo a b).piecewise γ γ') t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Proof state:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I ((Ioo a b).piecewise γ γ') t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
apply (hγ t hmem).congr_of_eventuallyEq

Result:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ (Ioo a b).piecewise γ γ' =ᶠ[𝓝 t] γ

Proof state:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ ∃ s ∈ 𝓝 t, EqOn ((Ioo a b).piecewise γ γ') γ s

Tactic:
refine ⟨Ioo a b, isOpen_Ioo.mem_nhds hmem, ?_⟩

Result:
case pos
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b a' b' : ℝ
hγ : IsIntegralCurveOn γ v (Ioo a b)
hγ' : IsIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ EqOn ((Ioo a b).piecewise γ γ') γ (Ioo a b)