-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurveOn_comp_add {dt : ℝ} :
    IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ (· + dt)) v (-dt +ᵥ s)

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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ γ = (γ ∘ 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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
t : ℝ
⊢ γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t

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
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)

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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ IsIntegralCurveOn γ v s

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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ s = - -dt +ᵥ -dt +ᵥ s

Tactic:
simp only [neg_neg, vadd_neg_vadd]

Result:
no goals

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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
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:
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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ IsIntegralCurveOn γ v s

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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ γ = (γ ∘ 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
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ s)
⊢ s = - -dt +ᵥ -dt +ᵥ s