awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 ℝ ℝ)

Tactic:
⟨(continuous_add_const _).continuousWithinAt, ?_⟩

Premises used: continuous_add_const, And.intro, Continuous.continuousWithinAt, HasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
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)
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (M' := ℝ) (fun (x : ℝ) ↦ x + dt)
    ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t (ContinuousLinearMap.id ℝ ℝ)

Tactic:
refine ⟨(continuous_add_const _).continuousWithinAt, ?_⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
simp : HasFDerivWithinAt (fun (x : ℝ) ↦ x + dt) (ContinuousLinearMap.id ℝ ℝ) ((fun (x : ℝ) ↦ x + 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)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 (fun (x : ℝ) ↦ x + dt) (ContinuousLinearMap.id ℝ ℝ) ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t

Tactic:
(hasFDerivWithinAt_id _ _).add_const _

Premises used: instModuleTangentSpace._aux_1, HasFDerivWithinAt.add_const, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4, hasFDerivWithinAt_id
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 (fun (x : ℝ) ↦ x + dt) (ContinuousLinearMap.id ℝ ℝ) ((fun (x : ℝ) ↦ x + dt) ⁻¹' s) t

Tactic:
exact (hasFDerivWithinAt_id _ _).add_const _

Premises used: HasFDerivWithinAt.add_const, hasFDerivWithinAt_id
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩

Premises used: Iff.intro, IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
refine : ∀ (hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s}), IsMIntegralCurveOn γ v s
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v {t : ℝ | t + dt ∈ s} ↔ IsMIntegralCurveOn γ v s

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt) v
    {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} (t + -dt)}

Tactic:
hγ.comp_add (-dt)

Premises used: Neg.neg, IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
h₁ : s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} (t + -dt)}
⊢ IsMIntegralCurveOn γ v s

Tactic:
convert! hγ.comp_add (-dt)

Premises used: Neg.neg, IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt

Tactic:
ext t
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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}
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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}
⊢ s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t + dt ∈ s} (t + -dt)}

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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

Tactic:
simpa using isMIntegralCurveOn_comp_add (dt := -dt)

Premises used: isMIntegralCurveOn_comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
rw :
  ∀ (hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) (dt : ℝ),
    ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)

Tactic:
rw [isMIntegralCurveAt_iff'] at *

Premises used: isMIntegralCurveAt_iff'
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
obtain :
  ∀ (ε : ℝ) (hε : ε > 0) (h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)),
    ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
obtain ⟨ε, hε, h⟩ := hγ
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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) ε)

Tactic:
⟨ε, hε, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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₀ ε)
refine : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
refine ⟨ε, hε, ?_⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 {t : ℝ | t + dt ∈ Metric.ball t₀ ε}

Tactic:
h.comp_add dt

Premises used: IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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₁ : Metric.ball (t₀ - dt) ε = {t : ℝ | t + dt ∈ Metric.ball t₀ ε}
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
convert! h.comp_add dt

Premises used: IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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₀| < ε}
h₃ : Eq (α := Set ℝ) {y : ℝ | |y - t₀ + dt| < ε} {t : ℝ | |t + dt - t₀| < ε}
⊢ Eq (α := Set ℝ) {y : ℝ | dist y (t₀ - dt) < ε} {t : ℝ | t + dt ∈ Metric.ball t₀ ε}

Tactic:
simp_rw [Metric.mem_ball, Real.dist_eq, ← sub_add, add_sub_right_comm]

Premises used: sub_add, add_sub_right_comm, Metric.mem_ball, Real.dist_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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₀

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩

Premises used: Iff.intro, IsMIntegralCurveAt.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
refine : ∀ (hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt)), IsMIntegralCurveAt γ v t₀
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) v (t₀ - dt) ↔ IsMIntegralCurveAt γ v t₀

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt) v (t₀ - dt - -dt)

Tactic:
hγ.comp_add (-dt)

Premises used: IsMIntegralCurveAt.comp_add, Neg.neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
h₁ : t₀ = t₀ - dt - -dt
⊢ IsMIntegralCurveAt γ v t₀

Tactic:
convert! hγ.comp_add (-dt)

Premises used: IsMIntegralCurveAt.comp_add, Neg.neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt

Tactic:
ext t
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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)
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t

Tactic:
simp only [Function.comp_apply, neg_add_cancel_right]

Premises used: neg_add_cancel_right, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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)
⊢ t₀ = t₀ - dt - -dt

Tactic:
simp only [sub_neg_eq_add, sub_add_cancel]

Premises used: sub_add_cancel, sub_neg_eq_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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₀

Tactic:
simpa using isMIntegralCurveAt_comp_add (dt := -dt)

Premises used: isMIntegralCurveAt_comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
rw : ∀ (hγ : IsMIntegralCurveOn γ v univ) (dt : ℝ), IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v univ
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v

Tactic:
rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *

Premises used: isMIntegralCurve_iff_isMIntegralCurveOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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γ : IsMIntegralCurveOn γ v univ
dt : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) v univ

Tactic:
simpa using hγ.comp_add dt

Premises used: IsMIntegralCurveOn.comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩

Premises used: IsMIntegralCurve.comp_add, Iff.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 : ℝ
refine : ∀ (hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v), IsMIntegralCurve γ v
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) v ↔ IsMIntegralCurve γ v

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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 (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt) v

Tactic:
hγ.comp_add (-dt)

Premises used: IsMIntegralCurve.comp_add, Neg.neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
⊢ IsMIntegralCurve γ v

Tactic:
convert! hγ.comp_add (-dt)

Premises used: IsMIntegralCurve.comp_add, Neg.neg
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt

Tactic:
ext t
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t

Tactic:
simp only [Function.comp_apply, neg_add_cancel_right]

Premises used: neg_add_cancel_right, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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

Tactic:
simpa using isMIntegralCurve_comp_add (dt := -dt)

Premises used: isMIntegralCurve_comp_add
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
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
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)
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ x * a) {t : ℝ | t * a ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 ((a • v) ((γ ∘ fun (x : ℝ) ↦ x * a) t)))

Tactic:
rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.one_apply (R₁ := ℝ) a,
    ← ContinuousLinearMap.smulRight_comp_smulRight]

Premises used: ContinuousLinearMap.one_apply, ContinuousLinearMap.smulRight_comp_smulRight, Function.comp_apply, Pi.smul_apply