--- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun Jul 02 14:28:20 2023 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jul 03 11:45:59 2023 +0100
@@ -174,8 +174,8 @@
"(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
apply (rule compact_cbox convex_box)+
- unfolding interior_cbox
- apply (rule 1 2 3)+
+ unfolding interior_cbox image_subset_iff_funcset [symmetric]
+ apply (rule 1 2 3)+
apply blast
done
have "?F x \<noteq> 0"