-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma IsIntegralCurveOn.comp_add (hγ : IsIntegralCurveOn γ v s) (dt : ℝ) :
    IsIntegralCurveOn (γ ∘ (· + dt)) v (-dt +ᵥ 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
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x + dt) t
    (ContinuousLinearMap.smulRight 1 (v ((γ ∘ fun x => x + dt) t)))

Tactic:
rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]

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
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x + dt) t
    ((ContinuousLinearMap.smulRight 1 (v (γ (t + dt)))).comp (ContinuousLinearMap.id ℝ ℝ))

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

Tactic:
apply HasMFDerivAt.comp t (hγ (t + dt) 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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (fun x => x + dt) t (ContinuousLinearMap.id ℝ ℝ)

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
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x + dt) t
    ((ContinuousLinearMap.smulRight 1 (v (γ (t + dt)))).comp (ContinuousLinearMap.id ℝ ℝ))

Tactic:
rw [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm,
  ← mem_setOf (p := fun t ↦ t + dt ∈ s)] at 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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x + dt) t
    ((ContinuousLinearMap.smulRight 1 (v (γ (t + dt)))).comp (ContinuousLinearMap.id ℝ ℝ))

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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (fun x => x + dt) t (ContinuousLinearMap.id ℝ ℝ)

Tactic:
refine ⟨(continuous_add_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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasFDerivWithinAt (writtenInExtChartAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun x => x + dt)
    (ContinuousLinearMap.id ℝ ℝ) (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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasFDerivAt (fun x => x + dt) (ContinuousLinearMap.id ℝ ℝ) t

Tactic:
exact (hasFDerivAt_id _).add_const _

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
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun x => x + dt) v (-dt +ᵥ 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
dt t : ℝ
ht : t ∈ -dt +ᵥ s
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun x => x + dt) t
    (ContinuousLinearMap.smulRight 1 (v ((γ ∘ 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 ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasFDerivWithinAt (writtenInExtChartAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun x => x + dt)
    (ContinuousLinearMap.id ℝ ℝ) (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
dt t : ℝ
ht : t ∈ {x | x + dt ∈ s}
⊢ HasFDerivAt (fun x => x + dt) (ContinuousLinearMap.id ℝ ℝ) t