mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ -a < 0

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -(asup + ε / 2) < asup - ε / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -ε + (asup - ε / 2) < asup - ε / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ asup - ε / 2 < ε + (asup - ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -a < asup - ε / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case left.left
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂✝ : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂✝ : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ -(T + S) < t

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case left.right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂✝ : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂✝ : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ t < T + S

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case right.left
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂✝ : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂✝ : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ -(T + S) < t₀

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case right.right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurve γ v
hγ' : IsMIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂✝ : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂✝ : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ t₀ < T + S

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -ε + (asup - ε / 2) < a

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ asup + ε / 2 ≤ ε + (asup - ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -(asup - ε / 2) < a

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -ε - (asup - ε / 2) < -(asup - ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -(asup - ε / 2) < ε - (asup - ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -ε - (asup - ε / 2) ≤ -(asup + ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -a < ε - (asup - ε / 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range ↑I ×ˢ range ↑I') (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ (fderivWithin 𝕜 φ (range ↑I') (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).2 ∘SL
        fderivWithin 𝕜 Prod.snd (range ↑I ×ˢ range ↑I')
          (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)))
      (p.1.snd, p.2.snd) =
    (fderivWithin 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))) p.2.snd

Tactic:
simp [fderivWithin_snd, U]

Goal state after: