-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurveAt_comp_add {dt : ℝ} :
    IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ IsIntegralCurveAt γ v t₀

Tactic:
convert hγ.comp_add (-dt)

Result:
case h.e'_10
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt

case h.e'_12
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ t₀ = t₀ - dt - -dt

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)

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

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ IsIntegralCurveAt γ v t₀

Proof state:
case h.e'_10.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
t : ℝ
⊢ γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t

Tactic:
simp only [Function.comp_apply, neg_add_cancel_right]

Result:
no goals

Proof state:
case h.e'_12
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ t₀ = t₀ - dt - -dt

Tactic:
simp only [sub_neg_eq_add, sub_add_cancel]

Result:
no goals

Proof state:
case h.e'_10
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
⊢ γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt

Tactic:
ext t

Result:
case h.e'_10.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
t : ℝ
⊢ γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t