awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
⊢ -(asup + ε / 2) < 0
have linarith₁ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(asup + ε / 2) < 0
have linarith₂ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₄ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
⊢ -(asup + ε / 2) < 0
have linarith₆ : 0 ≤ -(asup + ε / 2) → 3 * (0 - ε) + 2 * (ε - asup) + (HMul.hMul (α := ℝ) 2 0 - -(2 * asup + 1 * ε)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₄ : 0 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : 0 ≤ -(asup + ε / 2) → 3 * (0 - ε) + 2 * (ε - asup) + (HMul.hMul (α := ℝ) 2 0 - -(2 * asup + 1 * ε)) = 0
⊢ -(asup + ε / 2) < 0
have linarith₇ : 0 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
⊢ 0 < a
have linarith : a ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : a ≤ 0 → 2 / 2 = 1
⊢ 0 < a
have linarith₁ : a ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : a ≤ 0 → 2 / 2 = 1
linarith₁ : a ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < a
have linarith₂ : a ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : a ≤ 0 → 2 / 2 = 1
linarith₁ : a ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < a
have linarith₃ : a ≤ 0 → 0 - ε + (2 * asup - 1 * ε - 2 * a) + 2 * (ε - asup) + 2 * (a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
⊢ -a < 0
have linarith : 0 ≤ -a → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -a → 2 / 2 = 1
⊢ -a < 0
have linarith₁ : 0 ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -a → 2 / 2 = 1
linarith₁ : 0 ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -a < 0
have linarith₂ : 0 ≤ -a → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
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
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 (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
linarith : 0 ≤ -a → 2 / 2 = 1
linarith₁ : 0 ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ -a → GT.gt (α := ℝ) 2 0
⊢ -a < 0
have linarith₃ : 0 ≤ -a → 0 - ε + (2 * asup - 1 * ε - 2 * a) + 2 * (ε - asup) + 2 * (0 - -a) = 0
Tactic: linarith