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
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
this : -(|t| + 1) < t ∧ t < |t| + 1
⊢ Ioo (-(|t| + 1)) (|t| + 1) ∈ 𝓝 t

Tactic:
Ioo_mem_nhds this.1 this.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
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
this : -(|t| + 1) < t ∧ t < |t| + 1
⊢ Ioo (-(|t| + 1)) (|t| + 1) ∈ 𝓝 t

Tactic:
exact Ioo_mem_nhds this.1 this.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
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⟩
x : M
⊢ (∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v) ↔
    ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun h ↦ ?_⟩

Premises used: IsMIntegralCurveOn, Exists, IsMIntegralCurve.isMIntegralCurveOn, _private.0.exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo.match_1, And, And.intro, Iff.intro, Exists.intro, OfNat.ofNat, Eq, Set.Ioo, Neg.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
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⟩
x : M
refine :
  ∀ (h : ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)),
    ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v
⊢ (∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v) ↔
    ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
refine ⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun 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
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⟩
x : M
h : ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
choose :
  ∀ (γ : (a : ℝ) → ℝ → M) (hγx : ∀ (a : ℝ), γ a 0 = x) (hγ : ∀ (a : ℝ), IsMIntegralCurveOn (γ a) v (Ioo (-a) a)),
    ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
choose γ hγx hγ using 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
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⟩
x : M
γ : (a : ℝ) → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ (a : ℝ), IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
⟨fun t ↦ γ (|t| + 1) t, hγx (|0| + 1),
    isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦  hγ a)⟩

Premises used: abs, HAdd.hAdd, And.intro, Exists.intro, isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo, OfNat.ofNat
-- 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
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⟩
x : M
γ : (a : ℝ) → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ (a : ℝ), IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
exact ⟨fun t ↦ γ (|t| + 1) t, hγx (|0| + 1),
    isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦  hγ a)⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
pos : ∀ (hmem : t ∈ Ioo a b), (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
neg : ∀ (hmem : t ∉ Ioo a b), (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t

Tactic:
by_cases hmem : t ∈ Ioo a b

Premises used: Set.Ioo
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∈ Ioo a b
pos : γ t = γ' t
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t

Tactic:
rw [piecewise, if_pos hmem]

Premises used: if_pos, Set.piecewise
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∈ Ioo a b
pos : t ∈ Ioo (max a a') (min b b')
⊢ γ t = γ' t

Tactic:
apply H
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∈ Ioo a b
⊢ t ∈ Ioo (max a a') (min b b')

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

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∉ Ioo a b
neg : (if t ∈ Ioo a b then γ t else γ' t) = γ' t
neg₁ neg₂ : γ' 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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
suffices : EqOn γ γ' (Ioo (max a a') (min b b'))
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t

Tactic:
suffices H : EqOn γ γ' (Ioo (max a a') (min b b')) by
    by_cases hmem : t ∈ Ioo a b
    · rw [piecewise, if_pos hmem]
      apply H
      simp [ht.1, ht.2, hmem.1, hmem.2]
    · rw [piecewise, if_neg hmem]
-- 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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
apply : t₀ ∈ Ioo (max a a') (min b b')
⊢ EqOn γ γ' (Ioo (max a a') (min b b'))

Tactic:
apply isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
    (hγ.mono (Ioo_subset_Ioo (le_max_left ..) (min_le_left ..)))
    (hγ'.mono (Ioo_subset_Ioo (le_max_right ..) (min_le_right ..))) h

Premises used: le_max_right, IsMIntegralCurveOn.mono, min_le_left, min_le_right, isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless, le_max_left, 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
⊢ t₀ ∈ Ioo (max a a') (min b b')

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

Premises used: Set.Mem, setOf, lt_min, max_lt, And.right, And.left, And.intro, 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
t₀ : ℝ
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')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
⊢ t₀ ∈ Ioo (max a a') (min b b')

Tactic:
exact ⟨max_lt ht₀.1.1 ht₀.2.1, lt_min ht₀.1.2 ht₀.2.2⟩
-- 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'
pos :
  ∀ (hmem : t ∈ Ioo a b),
    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)))
neg :
  ∀ (hmem : t ∉ Ioo a b),
    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)))
⊢ 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:
by_cases hmem : t ∈ Ioo a b

Premises used: 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 ∪ Ioo a' b'
hmem : t ∈ Ioo a b
pos :
  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_pos hmem]

Premises used: if_pos, Set.piecewise
-- 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
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_pos hmem]

Premises used: if_pos, Set.piecewise
-- 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
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 hmem |>.hasMFDerivAt (Ioo_mem_nhds hmem.1 hmem.2) |>.hasMFDerivWithinAt
      (s := Ioo a b ∪ Ioo a' b') |>.congr_of_eventuallyEq _ (by rw [piecewise, if_pos 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 ∪ Ioo a' b'
hmem : t ∈ 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 ∪ Ioo a' b'
hmem : t ∈ Ioo a b
x : ℝ
ht' : x ∈ Ioo a b
rw : (if x ∈ Ioo a b then γ x else γ' x) = γ x
rw₁ rw₂ : γ x = γ x
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' x = γ x

Tactic:
rw [piecewise, if_pos ht']

Premises used: if_pos, Set.piecewise
-- 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
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, ?_, fun _ ht' ↦ by rw [piecewise, if_pos 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
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 ∪ Ioo a' b'
hmem : t ∈ Ioo a b
⊢ Ioo a b ∈ 𝓝 t

Tactic:
Ioo_mem_nhds hmem.1 hmem.2

Premises used: Set.Mem, Ioo_mem_nhds, And.right, And.left