src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

 lemma homeomorphic_compact:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
     (* class constraint due to continuous_on_inverse *)
   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
-  unfolding homeomorphic_def by(metis homeomorphism_compact)
+  unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
 
 text{* Preservation of topological properties.                                   *}
 
 lemma homeomorphic_compactness:
  "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)"