src/HOL/Analysis/Further_Topology.thy

   have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
     by (fastforce simp: assms(2) subspace_mul)
   obtain c where homhc: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
     apply (rule_tac c="-d" in that)
     apply (rule homotopic_with_eq)
-       apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T])
+       apply (rule homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T])
     using d apply (auto simp: h_def)
     done
   show ?thesis
     apply (rule_tac x=c in exI)
     apply (rule homotopic_with_trans [OF _ homhc])
     apply (rule homotopic_with_eq)
-       apply (rule homotopic_compose_continuous_left [OF homfg conT0 sub0T])
+       apply (rule homotopic_with_compose_continuous_left [OF homfg conT0 sub0T])
       apply (auto simp: h_def)
     done
 qed
 
 

       by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
     show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
       using fim him by force
   qed auto
   then have "homotopic_with_canon (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
-    by (rule homotopic_compose_continuous_left [OF _ contk kim])
+    by (rule homotopic_with_compose_continuous_left [OF _ contk kim])
   then have "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
     apply (rule homotopic_with_eq, auto)
     by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
   then show ?thesis
     by (metis that)