diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Analysis/Smooth_Paths.thy
--- a/src/HOL/Analysis/Smooth_Paths.thy	Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Analysis/Smooth_Paths.thy	Tue Jan 31 14:05:16 2023 +0000
@@ -270,6 +270,9 @@
 lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
   by (metis closed_path_image valid_path_imp_path)
 
+lemma valid_path_translation_eq: "valid_path ((+)d \<circ> p) \<longleftrightarrow> valid_path p"
+  by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq)
+ 
 lemma valid_path_compose:
   assumes "valid_path g"
       and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
@@ -312,9 +315,8 @@
   ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
     using C1_differentiable_on_eq by blast
   moreover have "path (f \<circ> g)"
-    apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
     using der
-    by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
+    by (simp add: path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]] continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     using \<open>finite S\<close> by auto
 qed