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
rw :
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2 0 =
    x
⊢ γ_ext 0 = x
have rw₁ : (if 0 ∈ Ioo (-(asup + ε / 2)) a then (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 else γ2 0) = x
Tactic: rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise,
      if_pos ⟨by linarith, by linarith⟩, h0]
-- 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
rw :
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2 0 =
    x
rw₁ : (if 0 ∈ Ioo (-(asup + ε / 2)) a then (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 else γ2 0) = x
⊢ γ_ext 0 = x
have rw₂ : (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 = x
Tactic: rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise,
      if_pos ⟨by linarith, by linarith⟩, h0]
-- 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
rw :
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2 0 =
    x
rw₁ : (if 0 ∈ Ioo (-(asup + ε / 2)) a then (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 else γ2 0) = x
rw₂ : (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 = x
⊢ γ_ext 0 = x
have rw₃ : (if 0 ∈ Ioo (-a) a then γ 0 else γ1 0) = x
Tactic: rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise,
      if_pos ⟨by linarith, by linarith⟩, h0]
-- 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
rw :
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2 0 =
    x
rw₁ : (if 0 ∈ Ioo (-(asup + ε / 2)) a then (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 else γ2 0) = x
rw₂ : (Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1 0 = x
rw₃ : (if 0 ∈ Ioo (-a) a then γ 0 else γ1 0) = x
rw₄ : γ 0 = x
⊢ γ_ext 0 = x
have rw₅ : x = x
Tactic: rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise,
      if_pos ⟨by linarith, by linarith⟩, h0]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (hypothesis)
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
⊢ False
have heq_ext : γ_ext 0 = x
Tactic: have heq_ext : γ_ext 0 = x := by
    rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise,
      if_pos ⟨by linarith, by linarith⟩, h0]
-- 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
heq_ext : γ_ext 0 = x
⊢ False
have suffices : IsMIntegralCurveOn γ_ext v (Ioo (-(asup + ε / 2)) (asup + ε / 2))
Tactic: suffices hext : IsMIntegralCurveOn γ_ext v (Ioo (-(asup + ε / 2)) (asup + ε / 2)) from
    (not_lt.mpr <| le_csSup hbdd ⟨γ_ext, heq_ext, hext⟩) <| lt_add_of_pos_right asup (half_pos hε)
-- 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
heq_ext : γ_ext 0 = x
⊢ -(asup + ε / 2) < asup - ε / 2
have linarith : asup - ε / 2 ≤ -(asup + ε / 2) → 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
heq_ext : γ_ext 0 = x
linarith : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
⊢ -(asup + ε / 2) < asup - ε / 2
have linarith₁ : asup - ε / 2 ≤ -(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
heq_ext : γ_ext 0 = x
linarith : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₃ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(asup + ε / 2) < asup - ε / 2
have linarith₄ : asup - ε / 2 ≤ -(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
heq_ext : γ_ext 0 = x
linarith : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₃ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : asup - ε / 2 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₅ : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₆ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : asup - ε / 2 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
⊢ -(asup + ε / 2) < asup - ε / 2
have linarith₈ : asup - ε / 2 ≤ -(asup + ε / 2) → 4 * (0 - ε) + 4 * (ε - asup) + (2 * asup - 1 * ε - -(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
heq_ext : γ_ext 0 = x
linarith : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₁ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₃ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : asup - ε / 2 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₅ : asup - ε / 2 ≤ -(asup + ε / 2) → 2 / 2 = 1
linarith₆ : asup - ε / 2 ≤ -(asup + ε / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : asup - ε / 2 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 2 0
linarith₈ : asup - ε / 2 ≤ -(asup + ε / 2) → 4 * (0 - ε) + 4 * (ε - asup) + (2 * asup - 1 * ε - -(2 * asup + 1 * ε)) = 0
⊢ -(asup + ε / 2) < asup - ε / 2
have linarith₉ : asup - ε / 2 ≤ -(asup + ε / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith