awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' 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 ∈ 𝓝 t

Tactic:
exact Ioo_mem_nhds hmem.1 hmem.2

Premises used: Ioo_mem_nhds, And.right, And.left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' 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
⊢ t ∈ Ioo a b ∪ Ioo a' b'

Tactic:
have ht' := ht
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' 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
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ t ∉ Ioo a b → t ∈ Ioo a' b'

Tactic:
rw [mem_union, or_iff_not_imp_left] at ht

Premises used: Set.mem_union, Classical.or_iff_not_imp_left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' 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
ht' : t ∈ Ioo a b ∪ Ioo a' b'
ht₁ : t ∉ Ioo a b → t ∈ Ioo a' b'
⊢ t ∉ Ioo a b

Tactic:
rw [mem_union, or_iff_not_imp_left] at ht

Premises used: Set.mem_union, Classical.or_iff_not_imp_left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' 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
ht' : t ∈ Ioo a b ∪ Ioo a' b'
ht₁ : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem₁ : t ∉ Ioo a b
⊢ t ∈ Ioo a b ∪ Ioo a' b'

Tactic:
rw [mem_union, or_iff_not_imp_left] at ht

Premises used: Set.mem_union, Classical.or_iff_not_imp_left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
neg :
  HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ' t)))
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))

Tactic:
rw [piecewise, if_neg hmem]

Premises used: Set.piecewise, if_neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
rw : (if t ∈ Ioo a b then γ t else γ' t) = γ' t
rw₁ rw₂ : γ' t = γ' t
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t

Tactic:
rw [piecewise, if_neg hmem]

Premises used: Set.piecewise, if_neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
apply : (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' =ᶠ[𝓝[Ioo a b ∪ Ioo a' b'] t] γ'
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ' t)))

Tactic:
apply hγ' t (ht hmem) |>.hasMFDerivAt (Ioo_mem_nhds (ht hmem).1 (ht hmem).2)
      |>.hasMFDerivWithinAt (s := Ioo a b ∪ Ioo a' b')
      |>.congr_of_eventuallyEq _ (by rw [piecewise, if_neg hmem])

Premises used: Ioo_mem_nhds, HasMFDerivWithinAt.congr_of_eventuallyEq, HasMFDerivAt.hasMFDerivWithinAt, And.right, And.left, HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
rw : ∃ s ∈ 𝓝[Ioo a b ∪ Ioo a' b'] t, EqOn ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') γ' s
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' =ᶠ[𝓝[Ioo a b ∪ Ioo a' b'] t] γ'

Tactic:
rw [Filter.eventuallyEq_iff_exists_mem]

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ ∃ s ∈ 𝓝[Ioo a b ∪ Ioo a' b'] t, EqOn ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') γ' s

Tactic:
⟨Ioo a' b', ?_,
      eqOn_piecewise_of_isMIntegralCurveOn_Ioo hv hγ hγ' ht₀ h⟩

Premises used: And.intro, Exists.intro, eqOn_piecewise_of_isMIntegralCurveOn_Ioo, Set.Ioo
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
refine : Ioo a' b' ∈ 𝓝[Ioo a b ∪ Ioo a' b'] t
⊢ ∃ s ∈ 𝓝[Ioo a b ∪ Ioo a' b'] t, EqOn ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') γ' s

Tactic:
refine ⟨Ioo a' b', ?_,
      eqOn_piecewise_of_isMIntegralCurveOn_Ioo hv hγ hγ' ht₀ h⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
rw : Ioo a' b' ∈ 𝓝 t
⊢ Ioo a' b' ∈ 𝓝[Ioo a b ∪ Ioo a' b'] t

Tactic:
rw [(isOpen_Ioo.union isOpen_Ioo).nhdsWithin_eq ht']

Premises used: IsOpen.nhdsWithin_eq, isOpen_Ioo, IsOpen.union
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ Ioo a' b' ∈ 𝓝 t

Tactic:
Ioo_mem_nhds (ht hmem).1 (ht hmem).2

Premises used: Set.Mem, Ioo_mem_nhds, And.right, And.left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∉ Ioo a b → t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ Ioo a' b' ∈ 𝓝 t

Tactic:
exact Ioo_mem_nhds (ht hmem).1 (ht hmem).2

Premises used: Ioo_mem_nhds, And.right, And.left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ¬BddAbove s
⊢ ∀ (x : ℝ), ∃ y ∈ s, x < y

Tactic:
rw [not_bddAbove_iff] at hbdd

Premises used: not_bddAbove_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
rw : ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
rw [exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo hv]

Premises used: exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a : ℝ
obtain :
  ∀ (y : ℝ) (hlt : a < y) (γ : ℝ → M) (hγ1 : γ 0 = x) (hγ2 : IsMIntegralCurveOn γ v (Ioo (-y) y)),
    ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a y : ℝ
hlt : a < y
γ : ℝ → M
hγ1 : γ 0 = x
hγ2 : IsMIntegralCurveOn γ v (Ioo (-y) y)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩

Premises used: IsMIntegralCurveOn.mono, LT.lt.le, And.intro, Exists.intro, neg_le_neg, Set.Ioo_subset_Ioo
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a y : ℝ
hlt : a < y
γ : ℝ → M
hγ1 : γ 0 = x
hγ2 : IsMIntegralCurveOn γ v (Ioo (-y) y)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
suffices : ¬BddAbove s
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
suffices hbdd : ¬BddAbove s by
    rw [not_bddAbove_iff] at hbdd
    rw [exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo hv]
    intro a
    obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a
    exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
⊢ let asup := sSup s;
  asup = sSup s

Tactic:
set asup := sSup s with hasup

Premises used: SupSet.sSup
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
rw : 0 < ε / 2
⊢ -(ε / 2) < 0

Tactic:
rw [neg_lt, neg_zero]

Premises used: neg_lt, neg_zero
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
⊢ 0 < ε / 2

Tactic:
half_pos hε

Premises used: half_pos
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
⊢ 0 < ε / 2

Tactic:
exact half_pos hε

Premises used: half_pos
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
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
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
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ε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
obtain : ∀ (a : ℝ) (ha : a ∈ s) (hlt : sSup s + -(ε / 2) < a), False
⊢ False

Tactic:
obtain ⟨a, ha, hlt⟩ := Real.add_neg_lt_sSup (⟨ε, h x⟩ : Set.Nonempty s) (ε := - (ε / 2))
    (by rw [neg_lt, neg_zero]; exact half_pos hε)

Premises used: Real.add_neg_lt_sSup, Exists.intro