--- a/src/HOL/Analysis/Homeomorphism.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Oct 08 10:26:40 2019 +0000
@@ -533,9 +533,8 @@
unfolding f_def using \<open>norm b = 1\<close> norm_eq_1
by (force simp: field_simps inner_add_right inner_diff_right)
moreover have "f ` T \<subseteq> T"
- unfolding f_def using assms
- apply (auto simp: field_simps inner_add_right inner_diff_right)
- by (metis add_0 diff_zero mem_affine_3_minus)
+ unfolding f_def using assms \<open>subspace T\<close>
+ by (auto simp add: inner_add_right inner_diff_right mem_affine_3_minus subspace_mul)
moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)"
apply clarify
apply (rule_tac x = "g x" in image_eqI, auto)