-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma IsIntegralCurveAt.comp_add (hγ : IsIntegralCurveAt γ v t₀) (dt : ℝ) :
    IsIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt)

Proof state:
case intro.intro
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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
convert h.comp_add dt

Result:
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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε

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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε

Tactic:
rw [Metric.vadd_ball, vadd_eq_add, neg_add_eq_sub]

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
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)

Tactic:
rw [isIntegralCurveAt_iff'] at *

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₀ : ℝ
hγ : ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
dt : ℝ
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (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₀ : ℝ
hγ : ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
dt : ℝ
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
obtain ⟨ε, hε, h⟩ := hγ

Result:
case intro.intro
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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)

Proof state:
case intro.intro
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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)

Tactic:
refine ⟨ε, hε, ?_⟩

Result:
case intro.intro
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ε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)