From d08b04ea434e11f8dffc26a3b65c50e4f6ab921a Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Thu, 6 Jul 2023 17:23:29 +0200
Subject: [PATCH] bump

---
 leanpkg.toml                               | 2 +-
 src/caseI/statement.lean                   | 8 ++++++--
 src/number_theory/cyclotomic/cycl_rat.lean | 9 ++++-----
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/leanpkg.toml b/leanpkg.toml
index 875dcda1..5c10c7a3 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.51.1"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "fdc286cc6967a012f41b87f76dcd2797b53152af"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5dc6092d09e5e489106865241986f7f2ad28d4c8"}
diff --git a/src/caseI/statement.lean b/src/caseI/statement.lean
index 3bffa6bc..0b3f6550 100644
--- a/src/caseI/statement.lean
+++ b/src/caseI/statement.lean
@@ -110,7 +110,11 @@ begin
       (hpri.out.eq_two_or_odd.resolve_left $ λ h, by norm_num [h] at h5p) hζ'] at H₁,
   replace H₁ := congr_arg (λ x, span ({x} : set R)) H₁,
   simp only [← prod_span_singleton, ← span_singleton_pow] at H₁,
-  obtain ⟨I, hI⟩ := finset.exists_eq_pow_of_mul_eq_pow_of_coprime (λ η₁ hη₁ η₂ hη₂ hη, _) H₁ ζ hζ,
+  have hdom : is_domain (ideal (𝓞 (cyclotomic_field ⟨p, hpri.out.pos⟩ ℚ))) := ideal.is_domain,
+  let gcddom : gcd_monoid (ideal (𝓞 (cyclotomic_field ⟨p, hpri.out.pos⟩ ℚ))) :=
+    (ideal.normalized_gcd_monoid).to_gcd_monoid,
+  obtain ⟨I, hI⟩ := @finset.exists_eq_pow_of_mul_eq_pow_of_coprime _ _ _ hdom gcddom _ _ _ _ _
+    (λ η₁ hη₁ η₂ hη₂ hη, _) H₁ ζ hζ,
   { exact ⟨I, hI⟩ },
   { exact flt_ideals_coprime h5p H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI }
 end
@@ -147,7 +151,7 @@ begin
   obtain ⟨u, hu⟩ := hα,
   refine ⟨u⁻¹, α, _⟩,
   rw [← hu, mul_comm _ ↑u, ← mul_assoc],
-  simp
+  simp only [units.inv_mul, one_mul]
 end
 
 theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p)
diff --git a/src/number_theory/cyclotomic/cycl_rat.lean b/src/number_theory/cyclotomic/cycl_rat.lean
index 739cec4a..6ccc0c06 100644
--- a/src/number_theory/cyclotomic/cycl_rat.lean
+++ b/src/number_theory/cyclotomic/cycl_rat.lean
@@ -241,7 +241,7 @@ lemma flt_ideals_coprime2 [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y : ℤ} {η
   (hp : is_coprime x y) (hp2 : ¬ (p : ℤ) ∣ (x + y : ℤ) ) (hwlog : η₁ ≠ 1) :
   is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
 begin
-  let I := flt_ideals p x y hη₁ + flt_ideals p x y hη₂,
+  let I := flt_ideals p x y hη₁ ⊔ flt_ideals p x y hη₂,
   by_contra,
   have he := (not_coprime_not_top p (flt_ideals p x y hη₁)  (flt_ideals p x y hη₂)).1 h,
   have := exists_le_maximal I he,
@@ -267,8 +267,8 @@ begin
     apply this },
   have hel2 : ∃ v : Rˣ, (v : R) * x * (1 - η₁) ∈ I,
   { have : η₂ * (↑x + η₁ * ↑y) + -η₁ * (↑x + η₂ * ↑y) ∈ I := ideal.add_mem _
-      (mul_mem_left _ _ (mem_sup_left (mem_flt_ideals _ _ hη₁)))
-      (mul_mem_left _ _ (mem_sup_right (mem_flt_ideals _ _ _))),
+        (mul_mem_left _ _ (mem_sup_left (mem_flt_ideals x y hη₁)))
+        (mul_mem_left _ _ (mem_sup_right (mem_flt_ideals x y hη₂))),
     have h1 :  η₂ * (↑x + η₁ * ↑y) + -η₁ * (↑x + η₂ * ↑y) = (η₂ - η₁) * x, by ring,
     rw h1 at this,
     have hh := diff_of_roots2 ph hη₁ hη₂ hdiff hwlog,
@@ -291,8 +291,7 @@ begin
     have hvunit : is_unit (v : R), by {exact units.is_unit v, },
     apply (unit_mul_mem_iff_mem P hvunit).1 _,
     apply hP2,
-    apply hv,
-  },
+    apply hv },
   have hPrime:= hP1.is_prime,
   have hprime2 := is_prime.mem_or_mem hPrime hel11,
   have hprime3 := is_prime.mem_or_mem hPrime hel22,