awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
right : -(T + S) < t₀
right₁ : t₀ < T + S
⊢ t₀ ∈ Ioo (-(T + S)) (T + S)

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
linarith : t ≤ -(T + S) → -T - t + (0 - S) + (t - -(T + S)) = 0
⊢ -(T + S) < t

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
linarith : T + S ≤ t → t - T + (0 - S) + (T + S - t) = 0
⊢ t < T + S

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
linarith : t₀ ≤ -(T + S) → 0 - T + (-S - t₀) + (t₀ - -(T + S)) = 0
⊢ -(T + S) < t₀

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
linarith : T + S ≤ t₀ → 0 - T + (t₀ - S) + (T + S - t₀) = 0
⊢ t₀ < T + S

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂_1 : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂_1 : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T

Tactic:
exact ⟨T + S, by constructor <;> constructor <;> linarith⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t : ℝ
h₁ : ∀ (T : ℝ) (ht₀ : t ∈ Ioo (-T) T) (ht : t₀ ∈ Ioo (-T) T), γ t = γ' t
⊢ γ t = γ' t

Tactic:
obtain ⟨T, ht₀, ht⟩ : ∃ T, t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T := by
    obtain ⟨T, hT₁, hT₂⟩ := exists_abs_lt t
    obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂
    obtain ⟨S, hS₁, hS₂⟩ := exists_abs_lt t₀
    obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂
    exact ⟨T + S, by constructor <;> constructor <;> linarith⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
ht₀ : t ∈ Ioo (-T) T
ht : t₀ ∈ Ioo (-T) T
⊢ γ t = γ' t

Tactic:
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff ht (fun t _ ↦ hγt t) hv
    ((hγ.isMIntegralCurveOn _).mono (subset_univ _))
    ((hγ'.isMIntegralCurveOn _).mono (subset_univ _)) h ht₀

Premises used: isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, Set.subset_univ, IsMIntegralCurveOn.mono, IsMIntegralCurve.isMIntegralCurveOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
ht₀ : t ∈ Ioo (-T) T
ht : t₀ ∈ Ioo (-T) T
⊢ γ t = γ' t

Tactic:
exact isMIntegralCurveOn_Ioo_eqOn_of_contMDiff ht (fun t _ ↦ hγt t) hv
    ((hγ.isMIntegralCurveOn _).mono (subset_univ _))
    ((hγ'.isMIntegralCurveOn _).mono (subset_univ _)) h ht₀

Premises used: isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, Set.subset_univ, IsMIntegralCurveOn.mono, IsMIntegralCurve.isMIntegralCurveOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
⊢ γ = γ'

Tactic:
isMIntegralCurve_eq_of_contMDiff (fun _ ↦ BoundarylessManifold.isInteriorPoint) hv hγ hγ' h

Premises used: BoundarylessManifold.isInteriorPoint, isMIntegralCurve_eq_of_contMDiff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
a b : ℝ
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
heq : γ a = γ b
apply : (γ ∘ fun (x : ℝ) ↦ x + (a - b)) b = γ b
⊢ Periodic γ (a - b)

Tactic:
apply congrFun <|
    isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := b) hv (hγ.comp_add _) hγ _

Premises used: IsMIntegralCurve.comp_add, isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless, congrFun
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
a b : ℝ
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
heq : γ a = γ b
rw : γ (b + (a - b)) = γ b
rw₁ : γ a = γ b
rw₂ rw₃ : γ b = γ b
⊢ (γ ∘ fun (x : ℝ) ↦ x + (a - b)) b = γ b

Tactic:
rw [comp_apply, add_sub_cancel, heq]

Premises used: add_sub_cancel, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
rw : (∃ T > 0, Periodic γ T) ↔ ¬Injective γ
⊢ Xor (∃ T > 0, Periodic γ T) (Injective γ)

Tactic:
rw [xor_iff_iff_not]

Premises used: xor_iff_iff_not
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
⊢ (∃ T > 0, Periodic γ T) ↔ ¬Injective γ

Tactic:
⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩

Premises used: ne_of_gt, Function.Periodic.not_injective, Iff.intro, Function.Injective, Not, _private.0.IsMIntegralCurve.periodic_xor_injective.match_1
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
refine : ¬Injective γ → ∃ T > 0, Periodic γ T
⊢ (∃ T > 0, Periodic γ T) ↔ ¬Injective γ

Tactic:
refine ⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
h : ¬Injective γ
⊢ ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂

Tactic:
rw [Injective] at h

Premises used: Function.Injective
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
h : ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂
⊢ ∃ (a₁ : ℝ) (a₂ : ℝ), γ a₁ = γ a₂ ∧ a₁ ≠ a₂

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
h : ∃ (a₁ : ℝ) (a₂ : ℝ), γ a₁ = γ a₂ ∧ a₁ ≠ a₂
obtain : ∀ (a b : ℝ) (heq : γ a = γ b) (hne : a ≠ b), ∃ T > 0, Periodic γ T
⊢ ∃ T > 0, Periodic γ T

Tactic:
obtain ⟨a, b, heq, hne⟩ := h
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ ∃ T > 0, Periodic γ T

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

Premises used: abs, HSub.hSub, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne refine_1 : a ≠ b
⊢ |a - b| > 0

Tactic:
rw [gt_iff_lt, abs_pos, sub_ne_zero]

Premises used: sub_ne_zero, abs_pos, gt_iff_lt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ a ≠ b

Tactic:
hne
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ a ≠ b

Tactic:
exact hne
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
pos : ∀ (hab : a - b < 0), Periodic γ |a - b|
neg : ∀ (hab : 0 ≤ a - b), Periodic γ |a - b|
⊢ Periodic γ |a - b|

Tactic:
by_cases! hab : a - b < 0
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
pos : Periodic γ (b - a)
⊢ Periodic γ |a - b|

Tactic:
rw [abs_of_neg hab, neg_sub]

Premises used: neg_sub, abs_of_neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ (b - a)

Tactic:
hγ.periodic_of_eq hv heq.symm

Premises used: Eq.symm, IsMIntegralCurve.periodic_of_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, 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

Premises used: Eq.symm, IsMIntegralCurve.periodic_of_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
neg : Periodic γ (a - b)
⊢ Periodic γ |a - b|

Tactic:
rw [abs_of_nonneg hab]

Premises used: abs_of_nonneg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ (a - b)

Tactic:
hγ.periodic_of_eq hv heq

Premises used: IsMIntegralCurve.periodic_of_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ (a - b)

Tactic:
exact hγ.periodic_of_eq hv heq

Premises used: IsMIntegralCurve.periodic_of_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
rw :
  HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (t + dt))) ∘SL ContinuousLinearMap.id ℝ ℝ)
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((γ ∘ fun (x : ℝ) ↦ x + dt) t)))

Tactic:
rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]

Premises used: ContinuousLinearMap.smulRight, HAdd.hAdd, Function.comp_apply, OfNat.ofNat, ContinuousLinearMap.comp_id
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
apply :
  HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (M' := ℝ) (fun (x : ℝ) ↦ x + dt)
    ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t (ContinuousLinearMap.id ℝ ℝ)
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (t + dt))) ∘SL ContinuousLinearMap.id ℝ ℝ)

Tactic:
apply HasMFDerivWithinAt.comp t (hγ (t + dt) ht) _ subset_rfl

Premises used: HasMFDerivWithinAt.comp, subset_rfl