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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ Ioo (-a') a' ⊆ Ioo (-a) a
have ha : -a ≤ -a'
Tactic: apply Ioo_subset_Ioo
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ -a ≤ -a'
have linarith : -a' < -a → a' - a + (-a' - -a) = 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ a' ≤ a
have linarith : a < a' → a' - a + (a - a') = 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a t : ℝ
ht : t ∈ Ioo (-a) a
⊢ (fun (t : ℝ) ↦ γ (|t| + 1) t) t = γ a t
have pos : ∀ (hlt : |t| + 1 < a), (fun (t : ℝ) ↦ γ (|t| + 1) t) t = γ a t
Tactic: by_cases! hlt : |t| + 1 < a
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a t : ℝ
ht : t ∈ Ioo (-a) a
pos : ∀ (hlt : |t| + 1 < a), (fun (t : ℝ) ↦ γ (|t| + 1) t) t = γ a t
⊢ (fun (t : ℝ) ↦ γ (|t| + 1) t) t = γ a t
have neg : ∀ (hlt : a ≤ |t| + 1), (fun (t : ℝ) ↦ γ (|t| + 1) t) t = γ a t
Tactic: by_cases! hlt : |t| + 1 < a
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
⊢ t ∈ Ioo (-(|t| + 1)) (|t| + 1)
have rw : |t| < |t| + 1
Tactic: rw [mem_Ioo, ← abs_lt]
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I (fun (t : ℝ) ↦ γ (|t| + 1) t) t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((fun (t : ℝ) ↦ γ (|t| + 1) t) t)))
have ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
Tactic: have ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1) := by
    rw [mem_Ioo, ← abs_lt]
    exact lt_add_one _
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I (fun (t : ℝ) ↦ γ (|t| + 1) t) t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((fun (t : ℝ) ↦ γ (|t| + 1) t) t)))
have h : HasMFDerivAt 𝓘(ℝ, ℝ) I (γ (|t| + 1)) t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((fun (t : ℝ) ↦ γ (|t| + 1) t) t)))
Tactic: apply HasMFDerivAt.congr_of_eventuallyEq (f := γ (|t| + 1))
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
h :
  HasMFDerivAt 𝓘(ℝ, ℝ) I (γ (|t| + 1)) t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((fun (t : ℝ) ↦ γ (|t| + 1) t) t)))
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I (fun (t : ℝ) ↦ γ (|t| + 1) t) t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((fun (t : ℝ) ↦ γ (|t| + 1) t) t)))
have h₁ : (fun (t : ℝ) ↦ γ (|t| + 1) t) =ᶠ[𝓝 t] γ (|t| + 1)
Tactic: apply HasMFDerivAt.congr_of_eventuallyEq (f := γ (|t| + 1))
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ (fun (t : ℝ) ↦ γ (|t| + 1) t) =ᶠ[𝓝 t] γ (|t| + 1)
have h₁ : ∃ s ∈ 𝓝 t, EqOn (fun (t : ℝ) ↦ γ (|t| + 1) t) (γ (|t| + 1)) s
Tactic: rw [Filter.eventuallyEq_iff_exists_mem]
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ ∃ s ∈ 𝓝 t, EqOn (fun (t : ℝ) ↦ γ (|t| + 1) t) (γ (|t| + 1)) s
have h₁ : Ioo (-(|t| + 1)) (|t| + 1) ∈ 𝓝 t
Tactic: refine ⟨Ioo (-(|t| + 1)) (|t| + 1), ?_,
      eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx hγ⟩
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ Ioo (-(|t| + 1)) (|t| + 1) ∈ 𝓝 t
have this : |t| < |t| + 1
Tactic: have : |t| < |t| + 1 := lt_add_of_pos_right |t| zero_lt_one
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
this : |t| < |t| + 1
⊢ Ioo (-(|t| + 1)) (|t| + 1) ∈ 𝓝 t
have this₁ : -(|t| + 1) < t ∧ t < |t| + 1
Tactic: rw [abs_lt] at this
Cleared hypotheses: this
-- 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
⊢ (∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v) ↔
    ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
have refine : ∀ (h : ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)),
  ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v
Tactic: refine ⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun 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
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
x : M
h : ∀ (a : ℝ), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v
have choose : ∀ (γ : (a : ℝ) → ℝ → M) (hγx : ∀ (a : ℝ), γ a 0 = x) (hγ : ∀ (a : ℝ), IsMIntegralCurveOn (γ a) v (Ioo (-a) a)),
  ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v
Tactic: choose γ hγx hγ using h
Cleared hypotheses: 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_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have pos : ∀ (hmem : t ∈ Ioo a b), (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
Tactic: by_cases hmem : t ∈ Ioo a b
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
pos : ∀ (hmem : t ∈ Ioo a b), (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have neg : ∀ (hmem : t ∉ Ioo a b), (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
Tactic: by_cases hmem : t ∈ Ioo a b
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∈ Ioo a b
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have pos : γ t = γ' t
Tactic: rw [piecewise, if_pos hmem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∈ Ioo a b
⊢ γ t = γ' t
have pos : t ∈ Ioo (max a a') (min b b')
Tactic: apply 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_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∉ Ioo a b
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have neg : (if t ∈ Ioo a b then γ t else γ' t) = γ' t
Tactic: rw [piecewise, if_neg hmem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type u_2
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∉ Ioo a b
neg : (if t ∈ Ioo a b then γ t else γ' t) = γ' t
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have neg₁ : γ' t = γ' t
Tactic: rw [piecewise, if_neg hmem]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
⊢ (Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t = γ' t
have suffices : EqOn γ γ' (Ioo (max a a') (min b b'))
Tactic: suffices H : EqOn γ γ' (Ioo (max a a') (min b b')) by
    by_cases hmem : t ∈ Ioo a b
    · rw [piecewise, if_pos hmem]
      apply H
      simp [ht.1, ht.2, hmem.1, hmem.2]
    · rw [piecewise, if_neg hmem]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
⊢ EqOn γ γ' (Ioo (max a a') (min b b'))
have apply : t₀ ∈ Ioo (max a a') (min b b')
Tactic: apply isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
    (hγ.mono (Ioo_subset_Ioo (le_max_left ..) (min_le_left ..)))
    (hγ'.mono (Ioo_subset_Ioo (le_max_right ..) (min_le_right ..))) 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))
have pos : ∀ (hmem : t ∈ Ioo a b),
  HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))
Tactic: by_cases hmem : t ∈ Ioo a b
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
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⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
pos :
  ∀ (hmem : t ∈ Ioo a b),
    HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
      (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))
have neg : ∀ (hmem : t ∉ Ioo a b),
  HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ') (Ioo a b ∪ Ioo a' b') t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((Ioo a b).piecewise (β := fun (a : ℝ) ↦ M) γ γ' t)))
Tactic: by_cases hmem : t ∈ Ioo a b