-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurveAt_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
    IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· * a)) (a • v) (t₀ / a)

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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ IsIntegralCurveAt γ v t₀

Tactic:
convert hγ.comp_mul_ne_zero (inv_ne_zero ha)

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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ γ = (γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹

case h.e'_11
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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ v = a⁻¹ • a • v

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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ t₀ = t₀ / a / a⁻¹

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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ γ = (γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹

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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
t : ℝ
⊢ γ t = ((γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹) t

Proof state:
case h.e'_11
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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

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₀ a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)

Tactic:
refine ⟨fun hγ ↦ hγ.comp_mul_ne_zero ha, 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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ IsIntegralCurveAt γ v 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₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
⊢ t₀ = t₀ / a / a⁻¹

Tactic:
simp only [div_inv_eq_mul, div_mul_cancel₀ _ ha]

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
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
t : ℝ
⊢ γ t = ((γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹) t

Tactic:
simp only [Function.comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]

Result:
no goals