diff -r f3d19c8445ec -r 24b70433c2e8 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue May 30 12:07:48 2023 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Tue May 30 12:33:06 2023 +0100
@@ -3605,6 +3605,30 @@
         \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
   by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
 
+lemma homotopic_through_contractible_space:
+   "continuous_map X Y f \<and>
+        continuous_map X Y f' \<and>
+        continuous_map Y Z g \<and>
+        continuous_map Y Z g' \<and>
+        contractible_space Y \<and> path_connected_space Z
+        \<Longrightarrow> homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (g' \<circ> f')"
+  using nullhomotopic_through_contractible_space [of X Y f Z g]
+  using nullhomotopic_through_contractible_space [of X Y f' Z g']
+  by (metis continuous_map_const homotopic_constant_maps homotopic_with_imp_continuous_maps 
+      homotopic_with_trans path_connected_space_iff_path_component homotopic_with_sym)
+
+lemma homotopic_from_contractible_space:
+   "continuous_map X Y f \<and> continuous_map X Y g \<and>
+        contractible_space X \<and> path_connected_space Y
+        \<Longrightarrow> homotopic_with (\<lambda>x. True) X Y f g"
+  by (metis comp_id continuous_map_id homotopic_through_contractible_space)
+
+lemma homotopic_into_contractible_space:
+   "continuous_map X Y f \<and> continuous_map X Y g \<and>
+        contractible_space Y
+        \<Longrightarrow> homotopic_with (\<lambda>x. True) X Y f g"
+  by (metis continuous_map_id contractible_imp_path_connected_space homotopic_through_contractible_space id_comp)
+
 lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
    "contractible_space X \<longleftrightarrow>
         topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")