-- Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
/-- A global integral curve is injective xor periodic with positive period. -/
lemma IsIntegralCurve.periodic_xor_injective [BoundarylessManifold I M]
    (hγ : IsIntegralCurve γ v)
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) :
    Xor' (∃ T > 0, Periodic γ T) (Injective γ)

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ |a - b|

Tactic:
rw [abs_of_neg hab, neg_sub]

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ (b - a)

Proof state:
case intro.intro.intro.refine_2
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ Periodic γ |a - b|

Tactic:
by_cases hab : a - b < 0

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ |a - b|

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : ¬a - b < 0
⊢ Periodic γ |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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ (b - a)

Tactic:
exact hγ.periodic_of_eq hv heq.symm

Result:
no goals

Proof state:
case intro.intro.intro
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ ∃ T > 0, Periodic γ T

Tactic:
refine ⟨|a - b|, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ |a - b| > 0

case intro.intro.intro.refine_2
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ Periodic γ |a - b|

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ |a - b|

Tactic:
rw [abs_of_nonneg hab]

Result:
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
⊢ ¬Injective γ → ∃ T > 0, Periodic γ T

Tactic:
intro h

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
h : ¬Injective γ
⊢ ∃ T > 0, Periodic γ T