[STATEMENT]
lemma nullhomotopic_from_contractible_space:
  assumes f: "continuous_map X Y f" and X: "contractible_space X"
  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nullhomotopic_through_contractible_space [OF _ f X]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_map ?X X ?f; \<And>c. homotopic_with (\<lambda>h. True) ?X Y (f \<circ> ?f) (\<lambda>x. c) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c. homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis comp_id continuous_map_id)