awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
ha : a ∈ s
hlt : sSup s + -(ε / 2) < a
⊢ False
have ha₁ : ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
Tactic: rw [mem_setOf] at ha
Cleared hypotheses: ha, hlt
-- 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 : ℝ
ha : ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
hlt : sSup s + -(ε / 2) < a
⊢ False
have hlt₁ : asup - ε / 2 < a
Tactic: rw [← hasup, ← sub_eq_add_neg] at hlt
Cleared hypotheses: hlt
-- 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 : ℝ
ha : ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
hlt : asup - ε / 2 < a
⊢ False
have obtain : ∀ (γ : ℝ → M) (h0 : γ 0 = x) (hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)), False
Tactic: obtain ⟨γ, h0, hγ⟩ := ha
Cleared hypotheses: ha
-- 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)
⊢ False
have obtain : ∀ (γ1_aux : ℝ → M) (h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))) (hγ1 : IsMIntegralCurveOn γ1_aux v (Ioo (-ε) ε)), False
Tactic: obtain ⟨γ1_aux, h1_aux, hγ1⟩ := h (γ (-(asup - ε / 2)))
-- 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))
hγ1 : IsMIntegralCurveOn γ1_aux v (Ioo (-ε) ε)
⊢ False
have hγ1₁ : IsMIntegralCurveOn (γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)) v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
Tactic: rw [← isMIntegralCurveOn_comp_add (dt := asup - ε / 2)] at hγ1
Cleared hypotheses: hγ1
-- 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))
hγ1 : IsMIntegralCurveOn (γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)) v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
hγ1₁ :
  let γ1 : ℝ → M := γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2);
  IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
⊢ False
have γ1_def : let γ1 : ℝ → M := γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2);
γ1 = γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)
Tactic: set γ1 := γ1_aux ∘ (· + (asup - ε / 2)) with γ1_def
Cleared hypotheses: hγ1
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ1_def : γ1 = γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)
⊢ False
have heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
Tactic: have heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2)) := by simp [γ1_def, h1_aux]
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ1_def : γ1 = γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
⊢ False
have obtain : ∀ (γ2_aux : ℝ → M) (h2_aux : γ2_aux 0 = γ (asup - ε / 2)) (hγ2 : IsMIntegralCurveOn γ2_aux v (Ioo (-ε) ε)), False
Tactic: obtain ⟨γ2_aux, h2_aux, hγ2⟩ := h (γ (asup - ε / 2))
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ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)
hγ2 : IsMIntegralCurveOn γ2_aux v (Ioo (-ε) ε)
⊢ False
have hγ2₁ : IsMIntegralCurveOn (γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)) v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
Tactic: rw [← isMIntegralCurveOn_comp_sub (dt := asup - ε / 2)] at hγ2
Cleared hypotheses: hγ2
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ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)
hγ2 : IsMIntegralCurveOn (γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)) v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
hγ2₁ :
  let γ2 : ℝ → M := γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2);
  IsMIntegralCurveOn γ2 v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
⊢ False
have γ2_def : let γ2 : ℝ → M := γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2);
γ2 = γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)
Tactic: set γ2 := γ2_aux ∘ (· - (asup - ε / 2)) with γ2_def
Cleared hypotheses: hγ2
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ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)
hγ2 : IsMIntegralCurveOn γ2 v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
γ2_def : γ2 = γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)
⊢ False
have heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
Tactic: have heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2) := by simp [γ2_def, h2_aux]
-- 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)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ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)
hγ2 : IsMIntegralCurveOn γ2 v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
γ2_def : γ2 = γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
⊢ False
have hγ1₁ : IsMIntegralCurveOn γ1 v {t : ℝ | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
Tactic: simp_rw [Set.mem_Ioo, ← sub_lt_iff_lt_add, ← lt_sub_iff_add_lt, ← Set.mem_Ioo] at hγ1
Cleared hypotheses: hγ1
-- 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)
hγ2 : IsMIntegralCurveOn γ2 v {t : ℝ | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
γ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))}
⊢ False
have hγ2₁ : IsMIntegralCurveOn γ2 v {t : ℝ | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
Tactic: simp_rw [Set.mem_Ioo, lt_sub_iff_add_lt, sub_lt_iff_lt_add, ← Set.mem_Ioo] at hγ2
Cleared hypotheses: hγ2
-- 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))}
⊢ False
have hεle : ε ≤ asup
Tactic: have hεle : ε ≤ asup := le_csSup hbdd (h x)
-- 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
⊢ False
have γ_ext_def : let γ_ext :=
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2;
γ_ext =
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
Tactic: set γ_ext : ℝ → M := piecewise (Ioo (-(asup + ε / 2)) a)
    (piecewise (Ioo (-a) a) γ γ1) γ2 with γ_ext_def
-- 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
⊢ -(asup + ε / 2) < 0
have linarith : 0 ≤ -(asup + ε / 2) → 2 / 2 = 1
Tactic: linarith