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
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
apply : Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)
apply₁ : Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)
⊢ ∀ ⦃t : { x : ℝ // x ∈ Ioo a b }⦄
    (ht :
      Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
        (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t),
    Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t

Tactic:
apply IsClosed.closure_subset (isClosed_eq _ _)

Premises used: isClosed_eq, IsClosed.closure_subset
-- 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
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
rw :
  ∀ (x : { x : ℝ // x ∈ Ioo a b }), ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)) x
⊢ Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
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
apply : ContinuousAt γ (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
⊢ ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht)

Tactic:
apply ContinuousAt.comp _ continuousAt_subtype_val

Premises used: continuousAt_subtype_val, ContinuousAt.comp
-- 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
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
rw : ContinuousAt γ val
⊢ ContinuousAt γ (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)

Tactic:
rw [Subtype.coe_mk]

Premises used: Subtype.coe_mk
-- 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
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 γ val

Tactic:
hγ.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

Premises used: Ioo_mem_nhds, And.right, And.left, IsMIntegralCurveOn.continuousWithinAt, ContinuousWithinAt.continuousAt
-- 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
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 γ val

Tactic:
exact hγ.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

Premises used: Ioo_mem_nhds, And.right, And.left, IsMIntegralCurveOn.continuousWithinAt, ContinuousWithinAt.continuousAt
-- 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
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
rw :
  ∀ (x : { x : ℝ // x ∈ Ioo a b }), ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)) x
⊢ Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
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
apply : ContinuousAt γ' (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
⊢ ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht)

Tactic:
apply ContinuousAt.comp _ continuousAt_subtype_val

Premises used: continuousAt_subtype_val, ContinuousAt.comp
-- 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
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
rw : ContinuousAt γ' val
⊢ ContinuousAt γ' (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)

Tactic:
rw [Subtype.coe_mk]

Premises used: Subtype.coe_mk
-- 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
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 γ' val

Tactic:
hγ'.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

Premises used: Ioo_mem_nhds, And.right, And.left, IsMIntegralCurveOn.continuousWithinAt, ContinuousWithinAt.continuousAt
-- 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
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 γ' val

Tactic:
exact hγ'.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

Premises used: Ioo_mem_nhds, And.right, And.left, IsMIntegralCurveOn.continuousWithinAt, ContinuousWithinAt.continuousAt
-- 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
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
rw : ∀ x ∈ s, s ∈ 𝓝 x
⊢ IsOpen s

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- 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
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
⊢ Ioo a b ∈ 𝓝 t₁

Tactic:
have hmem := Ioo_mem_nhds ht₁.2.1 ht₁.2.2
-- 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
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₁
⊢ γ =ᶠ[𝓝 t₁] γ'

Tactic:
have heq : γ =ᶠ[𝓝 t₁] γ' := isMIntegralCurveAt_eventuallyEq_of_contMDiffAt
      (hγt _ ht₁.2) hv.contMDiffAt (hγ.isMIntegralCurveAt hmem) (hγ'.isMIntegralCurveAt hmem) ht₁.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
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₁] γ'
apply : ∀ (x : ℝ), γ x = γ' x ∧ a < x ∧ x < b → ({t : ℝ | γ t = γ' t} ∩ Ioo a b) x
⊢ s ∈ 𝓝 t₁

Tactic:
apply (heq.and hmem).mono

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- 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
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₁] γ'
⊢ ∀ (x : ℝ), γ x = γ' x ∧ a < x ∧ x < b → ({t : ℝ | γ t = γ' t} ∩ Ioo a b) x

Tactic:
fun _ ht ↦ ht

Premises used: Set.Mem, setOf, Set.inter, Set.Ioo
-- 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
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₁] γ'
⊢ ∀ (x : ℝ), γ x = γ' x ∧ a < x ∧ x < b → ({t : ℝ | γ t = γ' t} ∩ Ioo a b) x

Tactic:
exact fun _ ht ↦ 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
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₀
h₁ : ∀ (t : ℝ), γ t = γ' t
⊢ γ = γ'

Tactic:
ext t
-- 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 : ℝ
obtain : ∀ (T : ℝ) (hT₁ : T > 0) (hT₂ : |t| < T), ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := exists_abs_lt t

Premises used: exists_abs_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
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

Tactic:
obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂

Premises used: Iff.mp, abs_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
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

Tactic:
obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂

Premises used: Iff.mp, abs_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
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
obtain : ∀ (S : ℝ) (hS₁ : S > 0) (hS₂ : |t₀| < S), ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T
⊢ ∃ (T : ℝ), t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T

Tactic:
obtain ⟨S, hS₁, hS₂⟩ := exists_abs_lt t₀

Premises used: exists_abs_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
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
⊢ -S < t₀

Tactic:
obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂

Premises used: Iff.mp, abs_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
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₀ < S

Tactic:
obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂

Premises used: Iff.mp, abs_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
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)
right : t₀ ∈ Ioo (-(T + S)) (T + S)
⊢ t ∈ Ioo (-(T + S)) (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
left : -(T + S) < t
left₁ : t < T + S
⊢ t ∈ Ioo (-(T + S)) (T + S)

Tactic:
constructor