awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂
⊢ ∃ T > 0, Periodic γ T
have h₁ : ∃ (a₁ : ℝ) (a₂ : ℝ), γ a₁ = γ a₂ ∧ a₁ ≠ a₂
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ∃ (a₁ : ℝ) (a₂ : ℝ), γ a₁ = γ a₂ ∧ a₁ ≠ a₂
⊢ ∃ T > 0, Periodic γ T
have obtain : ∀ (a b : ℝ) (heq : γ a = γ b) (hne : a ≠ b), ∃ T > 0, Periodic γ T
Tactic: obtain ⟨a, b, heq, hne⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ Periodic γ |a - b|
have pos : ∀ (hab : a - b < 0), Periodic γ |a - b|
Tactic: by_cases! hab : a - b < 0
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ℝ
heq : γ a = γ b
hne : a ≠ b
pos : ∀ (hab : a - b < 0), Periodic γ |a - b|
⊢ Periodic γ |a - b|
have neg : ∀ (hab : 0 ≤ a - b), Periodic γ |a - b|
Tactic: by_cases! hab : a - b < 0
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ |a - b|
have pos : Periodic γ (b - a)
Tactic: rw [abs_of_neg hab, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
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 : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ |a - b|
have neg : Periodic γ (a - b)
Tactic: rw [abs_of_nonneg hab]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v ((γ ∘ fun (x : ℝ) ↦ x + dt) t)))
have rw : HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
  (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (t + dt))) ∘SL ContinuousLinearMap.id ℝ ℝ)
Tactic: rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x + dt) {t : ℝ | t + dt ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (t + dt))) ∘SL ContinuousLinearMap.id ℝ ℝ)
have apply : HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (M' := ℝ) (fun (x : ℝ) ↦ x + dt)
  ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t (ContinuousLinearMap.id ℝ ℝ)
Tactic: apply HasMFDerivWithinAt.comp t (hγ (t + dt) ht) _ subset_rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (M' := ℝ) (fun (x : ℝ) ↦ x + dt)
    ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t (ContinuousLinearMap.id ℝ ℝ)
have refine : HasFDerivWithinAt
  (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦ x + dt)
  (ContinuousLinearMap.id ℝ ℝ)
  ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹' (fun (x : ℝ) ↦ x + dt) ⁻¹' s ∩
    range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
  ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)
Tactic: refine ⟨(continuous_add_const _).continuousWithinAt, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} t
⊢ HasFDerivWithinAt
    (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦ x + dt)
    (ContinuousLinearMap.id ℝ ℝ)
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹' (fun (x : ℝ) ↦ x + dt) ⁻¹' s ∩
      range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)
have simp : HasFDerivWithinAt (fun (x : ℝ) ↦ x + dt) (ContinuousLinearMap.id ℝ ℝ) ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s} ↔ IsMIntegralCurveOn γ v s
have refine : ∀ (hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s}), IsMIntegralCurveOn γ v s
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s}
⊢ IsMIntegralCurveOn γ v s
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s}
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
⊢ IsMIntegralCurveOn γ v s
have h₁ : s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} (t + -dt)}
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s}
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγ : IsMIntegralCurveAt γ v t₀
dt : ℝ
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)
have rw : ∀ (hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) (dt : ℝ),
  ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
Tactic: rw [isMIntegralCurveAt_iff'] at *
Cleared hypotheses: hγ, dt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
dt : ℝ
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
have obtain : ∀ (ε : ℝ) (hε : ε > 0) (h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)),
  ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
Tactic: obtain ⟨ε, hε, h⟩ := hγ
Cleared hypotheses: hγ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
have refine : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
Tactic: refine ⟨ε, hε, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
have h₁ : Metric.ball (t₀ - dt) ε = {t : ℝ | t + dt ∈ Metric.ball t₀ ε}
Tactic: convert! h.comp_add dt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | t + dt ∈ Metric.ball t₀ ε}
have h₁ : Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | dist (t + dt) t₀ < ε}
Tactic: simp_rw [Metric.mem_ball, Real.dist_eq, ← sub_add, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
h₁ : Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | dist (t + dt) t₀ < ε}
⊢ Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | t + dt ∈ Metric.ball t₀ ε}
have h₂ : Eq (α := Set ℝ) {y : ℝ | |y - (t₀ - dt)| < ε} {t : ℝ | |t + dt - t₀| < ε}
Tactic: simp_rw [Metric.mem_ball, Real.dist_eq, ← sub_add, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
h₁ : Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | dist (t + dt) t₀ < ε}
h₂ : Eq (α := Set ℝ) {y : ℝ | |y - (t₀ - dt)| < ε} {t : ℝ | |t + dt - t₀| < ε}
⊢ Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | t + dt ∈ Metric.ball t₀ ε}
have h₃ : Eq (α := Set ℝ) {y : ℝ | |y - t₀ + dt| < ε} {t : ℝ | |t + dt - t₀| < ε}
Tactic: simp_rw [Metric.mem_ball, Real.dist_eq, ← sub_add, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt) ↔ IsMIntegralCurveAt γ v t₀
have refine : ∀ (hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)), IsMIntegralCurveAt γ v t₀
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)
⊢ IsMIntegralCurveAt γ v t₀
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
⊢ IsMIntegralCurveAt γ v t₀
have h₁ : t₀ = t₀ - dt - -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurve γ v
dt : ℝ
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v
have rw : ∀ (hγ : IsMIntegralCurveOn γ v univ) (dt : ℝ), IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v univ
Tactic: rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *
Cleared hypotheses: hγ, dt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v ↔ IsMIntegralCurve γ v
have refine : ∀ (hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v), IsMIntegralCurve γ v
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v
⊢ IsMIntegralCurve γ v
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x * a) {t : ℝ | t * a ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 ((a • v) ((γ ∘ fun (x : ℝ) ↦ x * a) t)))
have rw : HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
  {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
  (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ)))) ∘SL
    ContinuousLinearMap.smulRight (S := ℝ) 1 a)
Tactic: rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.one_apply (R₁ := ℝ) a,
    ← ContinuousLinearMap.smulRight_comp_smulRight]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ)))) ∘SL
      ContinuousLinearMap.smulRight (S := ℝ) 1 a)
have refine : HasFDerivWithinAt (𝕜 := ℝ)
  (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦
    HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
  (ContinuousLinearMap.smulRight (S := ℝ) 1 a)
  ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹'
      {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} ∩
    range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
  ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)
Tactic: refine HasMFDerivWithinAt.comp t (hγ (t * a) ht)
    ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasFDerivWithinAt (𝕜 := ℝ)
    (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦
      HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a)
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹'
        {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} ∩
      range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)
have simp : HasFDerivWithinAt (𝕜 := ℝ) (fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
  (ContinuousLinearMap.smulRight (S := ℝ) 1 a) {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s
have refine : ∀ (hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}), IsMIntegralCurveOn γ v s
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul a⟩