src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

 qed
 
 lemma closed_contains_Inf:
   fixes S :: "real set"
   shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
-  by (metis closure_contains_Inf closure_closed assms)
+  by (metis closure_contains_Inf closure_closed)
 
 lemma closed_subset_contains_Inf:
   fixes A C :: "real set"
   shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<in> C"
   by (metis closure_contains_Inf closure_minimal subset_eq)