# HG changeset patch
# User nipkow
# Date 1665505809 -7200
# Node ID 7aa2eb860db4a44c8361ca37bc4d21451a9cbb83
# Parent  26524d0b43959e11c705f8aeeb7208443a8242f0
adjusted proofs

diff -r 26524d0b4395 -r 7aa2eb860db4 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Tue Oct 11 14:22:11 2022 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Tue Oct 11 18:30:09 2022 +0200
@@ -163,12 +163,6 @@
     by (auto simp add: B_def inj_on_def A_def) metis
 qed
 
-lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
-  apply (auto simp add: E_def C_def B_def A_def)
-  apply (rule inj_on_inverseI [where g = "(-) (int p)"])
-  apply auto
-  done
-
 lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
   for x :: int
   by (simp add: cong_def)
@@ -241,7 +235,7 @@
   by (simp add: B_card_eq_A A_card_eq)
 
 lemma F_card_eq_E: "card F = card E"
-  using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
+  using finite_E by (simp add: F_def card_image)
 
 lemma C_card_eq_B: "card C = card B"
 proof -
@@ -312,11 +306,7 @@
 lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * prod id E] (mod p)"
 proof -
   have FE: "prod id F = prod ((-) p) E"
-    apply (auto simp add: F_def)
-    apply (insert finite_E inj_on_pminusx_E)
-    apply (drule prod.reindex)
-    apply auto
-    done
+    using finite_E prod.reindex[OF inj_on_diff_left] by (auto simp add: F_def)
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_def minus_mod_self1 mod_mod_trivial)
   then have "[prod ((\<lambda>x. x mod p) \<circ> ((-) p)) E = prod (uminus) E](mod p)"
@@ -356,7 +346,7 @@
     by simp
   then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
     by (rule cong_trans)
-      (simp add: cong_scalar_left cong_scalar_right finite_A prod_constant ac_simps)
+      (simp add: cong_scalar_left cong_scalar_right finite_A ac_simps)
   then have a: "[prod id A * (-1)^(card E) =
       ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
     by (rule cong_scalar_right)