-- Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean
/-- Let `γ` and `γ'` be integral curves defined on `Ioo a b` and `Ioo a' b'`, respectively. Then,
`piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains.
`Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality
for `γ'` by the uniqueness of integral curves. -/
lemma eqOn_piecewise_of_isIntegralCurveOn_Ioo [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'))
    (ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b') (h : γ t₀ = γ' t₀) :
    EqOn (piecewise (Ioo a b) γ γ') γ' (Ioo a' b')

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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
⊢ t₀ ∈ Ioo (a ⊔ a') (b ⊓ b')

Tactic:
exact ⟨max_lt ht₀.1.1 ht₀.2.1, lt_min ht₀.1.2 ht₀.2.2⟩

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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
⊢ (Ioo a b).piecewise γ γ' t = γ' t

Tactic:
by_cases hmem : t ∈ Ioo a b

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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ (Ioo a b).piecewise γ γ' t = γ' t

case neg
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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∉ Ioo a b
⊢ (Ioo a b).piecewise γ γ' t = γ' t

Proof state:
case pos.a
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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ t ∈ Ioo (a ⊔ a') (b ⊓ b')

Tactic:
simp [ht.1, ht.2, hmem.1, hmem.2]

Result:
no goals

Proof state:
case neg
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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∉ Ioo a b
⊢ (Ioo a b).piecewise γ γ' t = γ' t

Tactic:
rw [piecewise, if_neg hmem]

Result:
no goals

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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ (Ioo a b).piecewise γ γ' t = γ' 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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ γ t = γ' 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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ γ t = γ' t

Tactic:
apply H

Result:
case pos.a
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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (a ⊔ a') (b ⊓ b'))
hmem : t ∈ Ioo a b
⊢ t ∈ Ioo (a ⊔ a') (b ⊓ b')