src/HOL/Library/FuncSet.thy

 proof
   assume L: ?lhs
   then show ?rhs
     apply (rule_tac x="f \<circ> inv_into (Collect P) g" in exI)
     unfolding o_def
-    by (metis (mono_tags, hide_lams) f_inv_into_f imageI inv_into_into mem_Collect_eq)
+    by (metis (mono_tags, opaque_lifting) f_inv_into_f imageI inv_into_into mem_Collect_eq)
 qed auto
 
 lemma function_factors_left:
   "(\<forall>x y. (g x = g y) \<longrightarrow> (f x = f y)) \<longleftrightarrow> (\<exists>h. f = h \<circ> g)"
   using function_factors_left_gen [of "\<lambda>x. True" g f] unfolding o_def by blast