awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, 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γ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
val : ℝ
ht : val ∈ Ioo a b
⊢ ContinuousAt γ' (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
have rw : ContinuousAt γ' val
Tactic: rw [Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, 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γ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ IsOpen s
have rw : ∀ x ∈ s, s ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, 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γ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
⊢ s ∈ 𝓝 t₁
have hmem : Ioo a b ∈ 𝓝 t₁
Tactic: have hmem := Ioo_mem_nhds ht₁.2.1 ht₁.2.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, 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γ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
⊢ s ∈ 𝓝 t₁
have heq : γ =ᶠ[𝓝 t₁] γ'
Tactic: have heq : γ =ᶠ[𝓝 t₁] γ' := isMIntegralCurveAt_eventuallyEq_of_contMDiffAt
      (hγt _ ht₁.2) hv.contMDiffAt (hγ.isMIntegralCurveAt hmem) (hγ'.isMIntegralCurveAt hmem) ht₁.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, 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γ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
heq : γ =ᶠ[𝓝 t₁] γ'
⊢ s ∈ 𝓝 t₁
have apply : ∀ (x : ℝ), γ x = γ' x ∧ a < x ∧ x < b → ({t : ℝ | γ t = γ' t} ∩ Ioo a b) x
Tactic: apply (heq.and hmem).mono
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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₀
⊢ γ = γ'
have h₁ : ∀ (t : ℝ), γ t = γ' t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have obtain : ∀ (T : ℝ) (hT₁ : T > 0) (hT₂ : |t| < T), ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
Tactic: obtain ⟨T, hT₁, hT₂⟩ := exists_abs_lt t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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₂ : |t| < T
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have hT₃ : -T < t
Tactic: obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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₂ : |t| < T
hT₃ : -T < t
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have hT₄ : t < T
Tactic: obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have obtain : ∀ (S : ℝ) (hS₁ : S > 0) (hS₂ : |t₀| < S), ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
Tactic: obtain ⟨S, hS₁, hS₂⟩ := exists_abs_lt t₀
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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₂ : |t₀| < S
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have hS₃ : -S < t₀
Tactic: obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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₂ : |t₀| < S
hS₃ : -S < t₀
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
have hS₄ : t₀ < S
Tactic: obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 ∈ Ioo (-(T + S)) (T + S) ∧ t₀ ∈ Ioo (-(T + S)) (T + S)
have left : t ∈ Ioo (-(T + S)) (T + S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
left : t ∈ Ioo (-(T + S)) (T + S)
⊢ t ∈ Ioo (-(T + S)) (T + S) ∧ t₀ ∈ Ioo (-(T + S)) (T + S)
have right : t₀ ∈ Ioo (-(T + S)) (T + S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 ∈ Ioo (-(T + S)) (T + S)
have left : -(T + S) < t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
left : -(T + S) < t
⊢ t ∈ Ioo (-(T + S)) (T + S)
have left₁ : t < T + S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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₀ ∈ Ioo (-(T + S)) (T + S)
have right : -(T + S) < t₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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₀
⊢ t₀ ∈ Ioo (-(T + S)) (T + S)
have right₁ : t₀ < T + S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 + S) < t
have linarith : t ≤ -(T + S) → -T - t + (0 - S) + (t - -(T + S)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 + S
have linarith : T + S ≤ t → t - T + (0 - S) + (T + S - t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 + S) < t₀
have linarith : t₀ ≤ -(T + S) → 0 - T + (-S - t₀) + (t₀ - -(T + S)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 + S
have linarith : T + S ≤ t₀ → 0 - T + (t₀ - S) + (T + S - t₀) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 = γ' t
have h₁ : ∀ (T : ℝ) (ht₀ : t ∈ Ioo (-T) T) (ht : t₀ ∈ Ioo (-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⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ Periodic γ (a - b)
have apply : (γ ∘ fun (x : ℝ) ↦ x + (a - b)) b = γ b
Tactic: apply congrFun <|
    isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := b) hv (hγ.comp_add _) hγ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ (γ ∘ fun (x : ℝ) ↦ x + (a - b)) b = γ b
have rw : γ (b + (a - b)) = γ b
Tactic: rw [comp_apply, add_sub_cancel, heq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ (γ ∘ fun (x : ℝ) ↦ x + (a - b)) b = γ b
have rw₂ : γ b = γ b
Tactic: rw [comp_apply, add_sub_cancel, heq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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⟩
⊢ Xor (∃ T > 0, Periodic γ T) (Injective γ)
have rw : (∃ T > 0, Periodic γ T) ↔ ¬Injective γ
Tactic: rw [xor_iff_iff_not]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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 γ
have refine : ¬Injective γ → ∃ T > 0, Periodic γ T
Tactic: refine ⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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 γ
⊢ ∃ T > 0, Periodic γ T
have h₁ : ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂
Tactic: rw [Injective] at h
Cleared hypotheses: h