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

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

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

Tactic:
convert hγ.comp_mul a⁻¹

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

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

Tactic:
refine ⟨fun hγ ↦ hγ.comp_mul _, 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
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun x => x * a) (a • v)
⊢ IsIntegralCurve γ v