-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma IsIntegralCurveOn.comp_mul (hγ : IsIntegralCurveOn γ v s) (a : ℝ) :
    IsIntegralCurveOn (γ ∘ (· * a)) (a • v) { t | t * a ∈ s }

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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x * a) t
    ((ContinuousLinearMap.smulRight 1 (v (γ (t * a)))).comp (ContinuousLinearMap.smulRight 1 a))

Tactic:
refine HasMFDerivAt.comp t (hγ (t * a) ht) ⟨(continuous_mul_right _).continuousAt, ?_⟩

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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasFDerivWithinAt (writtenInExtChartAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun x => x * a)
    (ContinuousLinearMap.smulRight 1 a) (range ↑(modelWithCornersSelf ℝ ℝ))
    (↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) 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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasFDerivWithinAt (writtenInExtChartAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun x => x * a)
    (ContinuousLinearMap.smulRight 1 a) (range ↑(modelWithCornersSelf ℝ ℝ))
    (↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) t)

Tactic:
simp only [mfld_simps, hasFDerivWithinAt_univ]

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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasFDerivAt (fun x => x * a) (ContinuousLinearMap.smulRight 1 a) 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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x * a) t
    (ContinuousLinearMap.smulRight 1 ((a • v) ((γ ∘ fun x => x * a) t)))

Tactic:
rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.smulRight_comp]

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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x * a) t
    ((ContinuousLinearMap.smulRight 1 (v (γ (t * a)))).comp (ContinuousLinearMap.smulRight 1 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
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasFDerivAt (fun x => x * a) (ContinuousLinearMap.smulRight 1 a) t

Tactic:
exact HasFDerivAt.mul_const' (hasFDerivAt_id _) _

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 ℝ
hγ : IsIntegralCurveOn γ v s
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) {t | t * a ∈ s}

Tactic:
intros t ht

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 ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x * a) t
    (ContinuousLinearMap.smulRight 1 ((a • v) ((γ ∘ fun x => x * a) t)))