diff -r a037f01aedab -r 1bd3463e30b8 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri May 07 16:49:08 2021 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun May 09 05:48:50 2021 +0000
@@ -1114,9 +1114,14 @@
       moreover have "j < i \<or> i = j \<or> i < j" by arith
       moreover note i
       ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
-        unfolding enum_def[abs_def] b.enum_def[abs_def]
-        by (auto simp: fun_eq_iff swap_image i'_def
-                           in_upd_image inj_on_image_set_diff[OF inj_upd]) }
+        apply (simp only: fun_eq_iff enum_def b.enum_def flip: image_comp)
+        apply (cases \<open>i = j\<close>)
+         apply simp
+         apply (metis Suc_i' \<open>i \<le> n\<close> imageI in_upd_image lessI lessThan_iff lessThan_subset_iff less_irrefl_nat transpose_apply_second transpose_commute)
+        apply (subst transpose_image_eq)
+         apply (auto simp add: i'_def)
+        done
+      }
     note enum_eq_benum = this
     then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
       by (intro image_cong) auto