From fe2463d1e17f4b26b4c092206cf0464ecdc03177 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Mon, 29 Apr 2024 11:47:04 +0200
Subject: [PATCH] bump

---
 FltRegular/MayAssume/Lemmas.lean                | 3 +--
 FltRegular/NumberTheory/Cyclotomic/CyclRat.lean | 2 --
 FltRegular/NumberTheory/Hilbert92.lean          | 1 -
 lake-manifest.json                              | 2 +-
 4 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean
index 9b9dd5c7..7f103172 100644
--- a/FltRegular/MayAssume/Lemmas.lean
+++ b/FltRegular/MayAssume/Lemmas.lean
@@ -1,7 +1,6 @@
 import FltRegular.FltThree.FltThree
 import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.FieldTheory.Finite.Basic
-import Mathlib.Algebra.GCDMonoid.Div
 import FltRegular.NumberTheory.RegularPrimes
 
 open Int Finset
@@ -39,7 +38,7 @@ theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a *
       Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
       Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc]
   · simpa [gcd_eq_gcd_image, d] using
-      Finset.Int.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
+      Finset.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
   · simp only [mul_eq_zero] at habs
     rcases habs with ((Ha | Hb) | Hc)
     · exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
index 80ec6495..5a9d363c 100644
--- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -114,8 +114,6 @@ instance a3 : NumberField (CyclotomicField p ℚ) :=
 
 open IsPrimitiveRoot
 
-attribute [-instance] CharP.CharOne.subsingleton
-
 theorem nth_roots_prim [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) :
     IsPrimitiveRoot η p := by
   have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
index f812886a..952d31a7 100644
--- a/FltRegular/NumberTheory/Hilbert92.lean
+++ b/FltRegular/NumberTheory/Hilbert92.lean
@@ -733,7 +733,6 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
       congr
       rw [hE]
       field_simp
-      rw [mul_comm]
   rw [norm_eq_prod_pow_gen σ hσ, orderOf_eq_card_of_forall_mem_zpowers hσ,
     IsGalois.card_aut_eq_finrank, hKL]
   conv =>
diff --git a/lake-manifest.json b/lake-manifest.json
index f4d16e59..37e80fc4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "0e991536465f9d37d4c0f73e1d2dd7bcde989e80",
+   "rev": "e9bc16347b34a91a7498edb615179b5788bf1ed4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,