From fd67acd1f5482d6113831ff0943b38419fae49c8 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Wed, 8 May 2024 12:38:11 +0200
Subject: [PATCH] bump

---
 FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean | 12 ++----------
 FltRegular/ReadyForMathlib/PowerBasis.lean         |  2 +-
 lake-manifest.json                                 |  2 +-
 3 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
index 84a06d07..c3c74b12 100644
--- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -149,6 +149,7 @@ theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type _} [CommRing A] [IsDomai
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
 set_option synthInstance.maxHeartbeats 40000 in
+set_option maxHeartbeats 400000 in
 theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p)
     (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (x : ℕ) = l) :
     algebraMap (𝓞 K) (𝓞 K ⧸ I) l = ∑ x : Fin t, (f x : 𝓞 K ⧸ I) := by
@@ -324,6 +325,7 @@ lemma Units.coe_map_inv' {M N F : Type*} [Monoid M] [Monoid N] [FunLike F M N]
     ↑((Units.map (f : M →* N) m)⁻¹) = f ↑(m⁻¹ : Mˣ) :=
   m.coe_map_inv (f : M →* N)
 
+set_option synthInstance.maxHeartbeats 40000 in
 lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) :
   algebraMap (𝓞 K) (𝓞 K ⧸ I) ((u * (unitGalConj K p u)⁻¹) : _) = 1 := by
   have := Units.coe_map_inv' (N := 𝓞 K ⧸ I) (algebraMap (𝓞 K) (𝓞 K ⧸ I)) (unitGalConj K p u)
@@ -371,16 +373,6 @@ theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp
   apply hζ.two_not_mem_one_sub_zeta h
   rw [← Ideal.Quotient.eq_zero_iff_mem, map_two, ← neg_one_eq_one_iff_two_eq_zero, ← hμ', hμ]
 
--- Add to mathlib
-@[norm_cast]
-lemma NumberField.RingOfIntegers.eq_iff {K : Type*} [Field K] {x y : 𝓞 K} :
-    (x : K) = (y : K) ↔ x = y :=
-  NumberField.RingOfIntegers.ext_iff.symm
-instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : Algebra (𝓞 K) L :=
-  inferInstanceAs (Algebra (integralClosure _ _) L)
-instance {K L : Type*} [Field K] [Ring L] [Algebra K L] :  IsScalarTower (𝓞 K) K L :=
-  inferInstanceAs (IsScalarTower (integralClosure _ _) K L)
-
 -- this proof has mild coe annoyances rn
 theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Rˣ) :
     ∃ m : ℕ, u * (unitGalConj K p u)⁻¹ = (hζ.unit' ^ m) ^ 2 := by
diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
index 9271cefc..745c2d21 100644
--- a/FltRegular/ReadyForMathlib/PowerBasis.lean
+++ b/FltRegular/ReadyForMathlib/PowerBasis.lean
@@ -28,7 +28,7 @@ theorem exists_int_sModEq (x : 𝓞 K) :
       simp only [Subtype.coe_mk] at h
       simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
       exact hi h
-    simp only [Fin.val_mk, _root_.pow_zero, Int.smul_one_eq_coe, zsmul_eq_mul] at H
+    simp only [Fin.val_mk, _root_.pow_zero, zsmul_eq_mul] at H
     rw [← Finset.sum_finset_coe] at H
     conv_lhs at H =>
       congr
diff --git a/lake-manifest.json b/lake-manifest.json
index d28e1584..7e01501b 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": "f29aeabbcf73fa5947bc5388d02476cc8986734c",
+   "rev": "89b4b590b4938e14211b6296f8ecf0c1940cc999",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,