Squashed commit of the following:

commit 8a6aa79
Author: Riccardo Brasca <[email protected]>
Date:   Mon May 6 12:17:19 2024 +0200

    fix again

commit 2c7f85c
Author: Riccardo Brasca <[email protected]>
Date:   Mon May 6 12:12:52 2024 +0200

    bump again

commit 4a97d0c
Author: Riccardo Brasca <[email protected]>
Date:   Mon May 6 12:09:43 2024 +0200

    fix build

commit de3819e
Author: Riccardo Brasca <[email protected]>
Date:   Sun May 5 14:14:26 2024 +0200

    progress

commit 0400baa
Author: Riccardo Brasca <[email protected]>
Date:   Sun May 5 13:24:42 2024 +0200

    this is done

commit 2efb0a3
Author: Riccardo Brasca <[email protected]>
Date:   Sun May 5 12:03:10 2024 +0200

    better

commit 68c61b7
Author: Ruben Van de Velde <[email protected]>
Date:   Fri May 3 23:16:18 2024 +0200

    note

commit 9ab7b4f
Author: Riccardo Brasca <[email protected]>
Date:   Fri May 3 22:39:38 2024 +0200

    start

Author: riccardobrasca

FltRegular/CaseI/Statement.lean

@@ -138,15 +138,14 @@ theorem is_principal {a b c : ℤ} {ζ : R} (hreg : IsRegularPrime p) (hp5 : 5 
   · rwa [IsRegularPrime, IsRegularNumber] at hreg
   · exact hI
 
-set_option maxHeartbeats 400000 in
 theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime p)
     (hζ : IsPrimitiveRoot ζ p) (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (caseI : ¬↑p ∣ a * b * c)
     (H : a ^ p + b ^ p = c ^ p) :
     ∃ k₁ k₂ : Fin p,
       k₂ ≡ k₁ - 1 [ZMOD p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ (k₁ : ℕ) - ↑b * ζ ^ (k₂ : ℕ) := by
   let ζ' := (ζ : K)
   have hζ' : IsPrimitiveRoot ζ' P := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
-  have h : ζ = (hζ'.unit' : R) := by simp only [IsPrimitiveRoot.unit', SetLike.eta, Units.val_mk]
+  have h : ζ = (hζ'.unit' : R) := by rfl
   have hP : P ≠ (2 : ℕ+) := by
     intro hP
     rw [← PNat.coe_inj, PNat.mk_coe] at hP
@@ -170,17 +169,16 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
   convert hk using 3
   rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)]
   congr 2
-  · rw [← Subtype.coe_inj]
-    simp only [Fin.val_mk, SubsemiringClass.coe_pow, NumberField.Units.coe_zpow,
-      IsPrimitiveRoot.coe_unit'_coe]
-    refine' eq_of_div_eq_one _
+  · ext
+    simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe]
+    refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, sub_self]
-  · rw [← Subtype.coe_inj]
-    simp only [Fin.val_mk, SubsemiringClass.coe_pow, MulMemClass.coe_mul,
-      NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
-    refine' eq_of_div_eq_one _
+  · ext
+    simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow,
+      IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
+    refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
       zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,

FltRegular/CaseII/AuxLemmas.lean

@@ -13,8 +13,6 @@ variable {ζ : K} (hζ : IsPrimitiveRoot ζ p)
 open scoped BigOperators nonZeroDivisors NumberField
 open Polynomial
 
-instance : CharZero (𝓞 K) := SubsemiringClass.instCharZero (𝓞 K)
-
 instance foofoo [NumberField K] : IsDomain (Ideal (𝓞 K)) := by convert Ideal.isDomain (A := 𝓞 K)
 
 instance [NumberField K] : CancelMonoidWithZero (Ideal (𝓞 K)) :=

FltRegular/CaseII/InductionStep.lean

@@ -40,8 +40,6 @@ lemma zeta_sub_one_dvd : π ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by
   apply dvd_pow_self
   simp
 
-set_option synthInstance.maxHeartbeats 160000 in
-set_option maxHeartbeats 400000 in
 lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
@@ -55,15 +53,15 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   rw [Finset.prod_const, ← map_pow, Ideal.Quotient.eq_zero_iff_dvd] at h
   exact hζ.zeta_sub_one_prime'.dvd_of_dvd_pow h
 
-lemma div_one_sub_zeta_mem : (x + y * η : 𝓞 K) / (ζ - 1) ∈ 𝓞 K := by
+lemma div_one_sub_zeta_mem : IsIntegral ℤ ((x + y * η : 𝓞 K) / (ζ - 1)) := by
   obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η
   rw [e, mul_comm]
-  simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring,
-    AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, ne_eq]
+  simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe,
+    map_one]
   rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 def div_zeta_sub_one : nthRootsFinset p (𝓞 K) → 𝓞 K :=
-fun η ↦ ⟨(x + y * η) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
+fun η ↦ ⟨(x + y * η.1) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
 
 lemma div_zeta_sub_one_mul_zeta_sub_one (η) :
     div_zeta_sub_one hp hζ e η * (π) = x + y * η := by
@@ -83,7 +81,6 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
   rw [Ne, ← Subtype.ext_iff.not]
   exact hη
 
-set_option synthInstance.maxHeartbeats 40000 in
 lemma div_zeta_sub_one_Injective :
     Function.Injective (fun η ↦ Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η)) := by
   letI : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
@@ -153,13 +150,11 @@ lemma m_mul_c_mul_p : 𝔪 * 𝔠 η * 𝔭 = 𝔦 η := by
   rw [div_zeta_sub_one_dvd_gcd_spec, Ideal.span_singleton_mul_span_singleton,
     div_zeta_sub_one_mul_zeta_sub_one]
 
-set_option synthInstance.maxHeartbeats 40000 in
 lemma m_ne_zero : 𝔪 ≠ 0 := by
   simp_rw [Ne, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
   rintro ⟨rfl, rfl⟩
   exact hy (dvd_zero _)
 
-set_option synthInstance.maxHeartbeats 40000 in
 lemma p_ne_zero : 𝔭 ≠ 0 := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
@@ -286,7 +281,7 @@ lemma p_dvd_c_iff : 𝔭 ∣ (𝔠 η) ↔ η = η₀ := by
     ← Ideal.dvd_span_singleton, ← div_zeta_sub_one_dvd_gcd_spec (hy := hy),
     ← dvd_gcd_mul_iff_dvd_mul, gcd_comm, gcd_zeta_sub_one_eq_one hζ hy, one_mul]
 
-lemma p_pow_dvd_c_eta_zero_aux [DecidableEq K] :
+lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] :
   gcd (𝔭 ^ (m * p)) (∏ η in Finset.attach (nthRootsFinset p (𝓞 K)) \ {η₀}, 𝔠 η) = 1 := by
     rw [← Ideal.isCoprime_iff_gcd]
     apply IsCoprime.pow_left
@@ -395,7 +390,6 @@ lemma a_mul_denom_eq_a_zero_mul_num (hη : η ≠ η₀) :
   simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]
   rw [mul_comm (𝔞₀ : FractionalIdeal (𝓞 K)⁰ K), ← div_eq_div_iff,
     ← a_div_a_zero_eq hp hreg hζ e hy hz η hη, FractionalIdeal.spanSingleton_div_spanSingleton]
-  · rfl
   · intro ha
     rw [FractionalIdeal.coeIdeal_eq_zero] at ha
     apply not_p_div_a_zero hp hζ e hy hz
@@ -425,7 +419,6 @@ def associated_eta_zero_unit (hη : η ≠ η₀) : (𝓞 K)ˣ :=
 
 local notation "ε" => associated_eta_zero_unit hp hreg hζ e hy hz
 
-set_option synthInstance.maxHeartbeats 40000 in
 lemma associated_eta_zero_unit_spec (η) (hη : η ≠ η₀) :
     ε η hη * (x + y * η₀) * α η hη ^ (p : ℕ) = (x + y * η) * π ^ (m * p) * β η hη ^ (p : ℕ) := by
   rw [mul_assoc, mul_comm (ε η hη : 𝓞 K)]
@@ -457,7 +450,6 @@ lemma stuff (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀
   congr 1
   ring
 
-set_option maxHeartbeats 400000 in
 lemma exists_solution :
     ∃ (x' y' z' : 𝓞 K) (ε₁ ε₂ ε₃ : (𝓞 K)ˣ), ¬ π ∣ x' ∧ ¬ π ∣ y' ∧ ¬ π ∣ z' ∧
       ↑ε₁ * x' ^ (p : ℕ) + ε₂ * y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by
@@ -524,8 +516,6 @@ lemma exists_solution'_aux {ε₁ ε₂ : (𝓞 K)ˣ} (hx : ¬ π ∣ x)
   rw [neg_mul, (Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow,
     sub_neg_eq_add, mul_sub, mul_one, mul_comm x b, add_sub_sub_cancel, add_comm]
 
-set_option synthInstance.maxHeartbeats 160000 in
-set_option maxHeartbeats 400000 in
 lemma exists_solution' :
     ∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ),
       ¬ π ∣ y' ∧ ¬ π ∣ z' ∧ x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by

FltRegular/NumberTheory/Cyclotomic/CaseI.lean

@@ -33,11 +33,12 @@ theorem exists_int_sum_eq_zero'_aux (x y i : ℤ) :
   intGal (galConj K p) (x + y * ↑(hζ.unit' ^ i) : 𝓞 K) = x + y * (hζ.unit' ^ (-i) : (𝓞 K)ˣ) := by
   ext1
   rw [intGal_apply_coe]
-  push_cast
+  simp only [_root_.map_add, map_intCast, _root_.map_mul, AlgHom.coe_coe, zpow_neg, map_units_inv,
+    add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero]
   simp_rw [NumberField.Units.coe_zpow]
+  left
   push_cast
-  simp only [zpow_neg, _root_.map_add, map_intCast, _root_.map_mul, map_zpow₀, AlgHom.coe_coe,
-    galConj_zeta_runity hζ, add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero, inv_zpow]
+  simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg]
 
 theorem exists_int_sum_eq_zero' (hpodd : p ≠ 2) (hp : (p : ℕ).Prime) (x y i : ℤ) {u : (𝓞 K)ˣ}
     {α : 𝓞 K} (h : (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) = u * α ^ (p : ℕ)) :

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -154,9 +154,8 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη :
   have h2 := IsPrimitiveRoot.sub_one_norm_prime this (cyclotomic.irreducible_rat p.2) h0
   convert h
   ext
-  rw [RingOfIntegers.coe_algebraMap_norm]
-  norm_cast at h2
-  rw [h2]
+  rw [show (η : CyclotomicField p ℚ) - 1 = (η - 1 : _) by simp] at h2
+  rw [RingOfIntegers.coe_algebraMap_norm, h2]
   simp
 
 theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R)
@@ -191,8 +190,6 @@ theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} (
 noncomputable
 instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup
 
-set_option maxHeartbeats 300000 in
-set_option synthInstance.maxHeartbeats 80000 in
 lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
     (hη₁ : η₁ ∈ nthRootsFinset p R)
     (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y)
@@ -345,7 +342,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     ⟨x, lt_trans x.2 (pred_lt hp.out.ne_zero)⟩ := fun x => Fin.ext rfl
   let ζ' := (ζ : L)
   have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
-  have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by simp
+  have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl
   set b := hζ'.integralPowerBasis' with hb
   have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp.out,
     pred_eq_sub_one]
@@ -371,8 +368,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
   conv_lhs at hy =>
     congr; rfl; ext x
-    rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y,
-      ← sub_eq_add_neg]
+    rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg]
   norm_cast at hy
   rw [sum_sub_distrib] at hy
   replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨i, hi⟩)) hy
@@ -392,7 +388,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
   let ζ' := (ζ : L)
   have : Fact (p : ℕ).Prime := ⟨hp⟩
   have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
-  have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by simp
+  have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl
   have hlast : (Fin.castIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) =
       ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ := Fin.ext rfl
   have h : ∀ x, (Fin.castIso (succ_pred_prime hp)) (Fin.castSuccEmb x) =
@@ -424,8 +420,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
     rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
   conv_lhs at hy =>
     congr; rfl; ext x
-    rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y,
-      ← sub_eq_add_neg]
+    rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg]
   norm_cast at hy
   rw [sum_sub_distrib] at hy
   replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨j, hj⟩)) hy

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -88,14 +88,16 @@ theorem galConj_idempotent : (galConj K p).trans (galConj K p) = AlgEquiv.refl :
 variable (p)
 
 --generalize this
-theorem gal_map_mem {x : K} (hx : x ∈ RR) (σ : K →ₐ[ℚ] K) : σ x ∈ RR :=
+theorem gal_map_mem {x : K} (hx : IsIntegral ℤ x) (σ : K →ₐ[ℚ] K) : IsIntegral ℤ (σ x) :=
   map_isIntegral_int (σ.restrictScalars ℤ) hx
 
-theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : σ x ∈ RR := by simp [gal_map_mem]
+theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : IsIntegral ℤ (σ x) :=
+  gal_map_mem x.2 _
 
 /-- Restriction of `σ : K →ₐ[ℚ] K` to the ring of integers.  -/
 def intGal (σ : K →ₐ[ℚ] K) : RR →ₐ[ℤ] RR :=
-  ((σ.restrictScalars ℤ).restrictDomain RR).codRestrict RR (gal_map_mem_subtype σ)
+  ((σ.restrictScalars ℤ).restrictDomain RR).codRestrict (integralClosure ℤ K)
+  (gal_map_mem_subtype σ)
 
 @[simp]
 theorem intGal_apply_coe (σ : K →ₐ[ℚ] K) (x : RR) : (intGal σ x : K) = σ x :=
@@ -111,7 +113,7 @@ variable (K)
 def unitGalConj : RRˣ →* RRˣ :=
   unitsGal (galConj K p)
 
-theorem unitGalConj_spec (u : RRˣ) : galConj K p (u : 𝓞 K) = ↑(unitGalConj K p u : 𝓞 K) := rfl
+theorem unitGalConj_spec (u : RRˣ) : galConj K p u = unitGalConj K p u := rfl
 
 variable {K}
 
@@ -123,6 +125,4 @@ theorem unit_lemma_val_one (u : RRˣ) (φ : K →+* ℂ) :
   simp only [map_inv₀, Complex.abs_conj]
   rw [mul_inv_eq_one₀]
   intro h
-  simp only [_root_.map_eq_zero] at h
-  rw [← Subalgebra.coe_zero (𝓞 K), Subtype.coe_inj] at h
-  exact Units.ne_zero _ h
+  simp at h

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -179,6 +179,7 @@ lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) :
   · rw [mem_nthRootsFinset p.pos, ← map_pow, hζ.unit'_coe.pow_eq_one, map_one]
   · rw [mem_nthRootsFinset p.pos, hζ.unit'_coe.pow_eq_one]
 
+set_option synthInstance.maxHeartbeats 80000 in
 lemma zeta_sub_one_dvd_trace_sub_smul (x : 𝓞 K) :
     (hζ.unit' - 1 : 𝓞 K) ∣ Algebra.trace ℤ _ x - (p - 1 : ℕ) • x := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
@@ -226,7 +227,7 @@ lemma norm_add_one_smul_of_isUnit {K} [Field K] [NumberField K] {p : ℕ} (hpri
     apply Int.natAbs_eq_iff.mp
     apply (Int.cast_injective (α := ℚ)).comp Nat.cast_injective
     simp only [Int.cast_abs, Function.comp_apply, Nat.cast_one, Int.cast_one, ← Int.abs_eq_natAbs,
-      Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.norm_apply_coe]
+      Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.coe_norm]
   have : Algebra.norm ℤ (1 + (p : ℕ) • x) ≠ -1 := by
     intro e; apply hp
     obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x