bump

FltRegular/CaseI/Statement.lean

@@ -76,10 +76,10 @@ theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0)
   replace hqpri : Prime (q : ℤ) := prime_iff_natAbs_prime.2 (by simp [hqpri])
   obtain ⟨n, hn⟩ := hq
   have haq : ↑q ∣ a := by
-    obtain ⟨m, hm⟩ := Int.gcd_dvd_left a b
+    obtain ⟨m, hm⟩ := @Int.gcd_dvd_left a b
     exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
   have hbq : ↑q ∣ b := by
-    obtain ⟨m, hm⟩ := Int.gcd_dvd_right a b
+    obtain ⟨m, hm⟩ := @Int.gcd_dvd_right a b
     exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
   have hcq : ↑q ∣ c := by
     suffices ↑q ∣ c ^ p by exact hqpri.dvd_of_dvd_pow this
@@ -168,6 +168,7 @@ 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) :

FltRegular/CaseII/Statement.lean

@@ -93,14 +93,14 @@ theorem caseII {a b c : ℤ} {p : ℕ} [hpri : Fact p.Prime] (hreg : IsRegularPr
   obtain (ha|hb) := (Nat.prime_iff_prime_int.mp hpri.out).dvd_or_dvd hab
   · refine not_exists_Int_solution' hreg hodd ⟨b, -c, -a, ?_, ?_, ?_, ?_⟩
     · simp only [← hgcd, Finset.mem_singleton, Finset.mem_insert, neg_inj, Finset.gcd_insert, id_eq,
-        ← Int.coe_gcd, Int.gcd_neg_left, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
+        ← Int.coe_gcd, Int.neg_gcd, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
         Int.gcd_left_comm _ a]
     · rwa [dvd_neg]
     · rwa [ne_eq, neg_eq_zero]
     · simp [hodd'.neg_pow, ← e]
   · refine not_exists_Int_solution' hreg hodd ⟨-c, a, -b, ?_, ?_, ?_, ?_⟩
     · simp only [← hgcd, Finset.mem_singleton, Finset.mem_insert, neg_inj, Finset.gcd_insert, id_eq,
-        ← Int.coe_gcd, Int.gcd_neg_left, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
+        ← Int.coe_gcd, Int.neg_gcd, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
         Int.gcd_left_comm _ c]
     · rwa [dvd_neg]
     · rwa [ne_eq, neg_eq_zero]

FltRegular/FltThree/FltThree.lean

@@ -23,8 +23,8 @@ theorem exists_coprime {n : ℕ} (hn : 0 < n) {a b c : ℤ} (ha' : a ≠ 0) (hb'
       a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c' :=
   by
   set d := Int.gcd a b with hd'
-  obtain ⟨A, HA⟩ : ↑d ∣ a := Int.gcd_dvd_left a b
-  obtain ⟨B, HB⟩ : ↑d ∣ b := Int.gcd_dvd_right a b
+  obtain ⟨A, HA⟩ : ↑d ∣ a := @Int.gcd_dvd_left a b
+  obtain ⟨B, HB⟩ : ↑d ∣ b := @Int.gcd_dvd_right a b
   obtain ⟨C, HC⟩ : ↑d ∣ c :=
     by
     rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
@@ -257,7 +257,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
     intro d hdprime hddvdg
     rw [← Int.coe_nat_dvd] at hddvdg
     apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg']
-    exacts[Int.gcd_dvd_left _ _, Int.gcd_dvd_right _ _]
+    exacts[Int.gcd_dvd_left, Int.gcd_dvd_right]
   refine' ⟨k, hg, _⟩
   by_contra! H
   rw [← pow_mul_pow_sub _ H] at hg
@@ -274,12 +274,12 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
     have : 3 ∣ (g : ℤ) := by
       rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
       apply dvd_mul_right
-    exact dvd_trans this (Int.gcd_dvd_left _ _)
+    exact dvd_trans this Int.gcd_dvd_left
   apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp
   · rw [← Int.pow_dvd_pow_iff zero_lt_two] at hdvdp
     apply Prime.dvd_of_dvd_pow Int.prime_three
     rw [← mul_dvd_mul_iff_left (three_ne_zero' ℤ), ← pow_two, ← dvd_add_right hdvdp]
-    refine' dvd_trans _ (Int.gcd_dvd_right (2 * p) (p ^ 2 + 3 * q ^ 2))
+    refine' dvd_trans _ Int.gcd_dvd_right
     rw [← hg', hg, Int.ofNat_mul]
     apply dvd_mul_right
 
@@ -567,7 +567,7 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
     apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two
     · zify  at hgcd
       rw [← hgcd]
-      exact Int.gcd_dvd_left _ _
+      exact Int.gcd_dvd_left
     · norm_num
   have h3_ndvd_q : ¬3 ∣ q := by
     intro H

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -223,12 +223,9 @@ theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} (
   rw [Units.val_neg, neg_mul, ← hu]
   ring
 
-instance arg : IsDedekindDomain R :=
-  inferInstance
-
 instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup
-instance : AddCommMonoid R := AddCommGroup.toAddCommMonoid
 
+set_option maxHeartbeats 300000 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)

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -12,8 +12,8 @@ theorem PowerBasis.rat_hom_ext {S S' : Type _} [CommRing S] [hS : Algebra ℚ S]
     [hS' : Algebra ℚ S'] (pb : PowerBasis ℚ S) ⦃f g : S →+* S'⦄ (h : f pb.gen = g pb.gen) : f = g :=
   let f' := f.toRatAlgHom
   let g' := g.toRatAlgHom
-  FunLike.ext f g <| by
-    convert FunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
+  DFunLike.ext f g <| by
+    convert DFunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
 
 variable (K : Type _) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
 
@@ -72,7 +72,7 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K
     by
     rw [← Function.funext_iff]
     congr
-    rw [FunLike.coe_fn_eq]
+    rw [DFunLike.coe_fn_eq]
     apply (hζ.powerBasis ℚ).rat_hom_ext
     exact this.symm
   rw [conj_norm_one, galConj_zeta_runity hζ, map_inv₀]

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -159,7 +159,7 @@ theorem eq_one_mod_one_sub {A : Type _} [CommRing A] {t : A} :
 
 theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type _} [CommRing A] [IsDomain A] {ζ : A}
     (hζ : IsPrimitiveRoot ζ p) {μ : A} (hμ : μ ^ (p : ℕ) = 1) :
-    (@FunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by
+    (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by
   obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
@@ -290,10 +290,10 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
     simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg]
     rw [← Subtype.val_inj] at Hi
     simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, Submonoid.coe_mul,
-      Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, AddSubgroupClass.coe_neg,
+      Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, InvMemClass.coe_inv,
       OneMemClass.coe_one, neg_mul, one_mul] at Hi
     simp only [IsPrimitiveRoot.unit'_val_coe]
-    exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm Hi))
+    exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm (by simpa using Hi)))
   obtain ⟨m, k, hmk⟩ := H
   refine' ⟨m, k, _⟩
   have eq : ((⟨x, hx⟩ : R) : K) = x := rfl

FltRegular/NumberTheory/CyclotomicRing.lean

@@ -95,7 +95,7 @@ lemma exists_dvd_int (n : CyclotomicIntegers p) (hn : n ≠ 0) : ∃ m : ℤ, m
   rw [← map_dvd_iff (equiv p), map_intCast]
   convert RingOfIntegers.dvd_norm ℚ (equiv p n) using 1
   ext1
-  exact FunLike.congr_arg (algebraMap ℚ _) (Algebra.coe_norm_int (equiv p n))
+  exact DFunLike.congr_arg (algebraMap ℚ _) (Algebra.coe_norm_int (equiv p n))
 
 lemma adjoin_zeta : Algebra.adjoin ℤ {zeta p} = ⊤ := AdjoinRoot.adjoinRoot_eq_top
 

FltRegular/NumberTheory/Hilbert92.lean

@@ -9,16 +9,11 @@ open scoped NumberField nonZeroDivisors
 open FiniteDimensional
 open NumberField
 
-variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] -- [IsCyclotomicExtension {p} ℚ K]
+variable (p : ℕ+) {K : Type*} [Field K] [NumberField K]
 variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p)
 
 open FiniteDimensional BigOperators Finset
 open CyclotomicIntegers (zeta)
--- Z[H] module M (rank L) submodule N (rank l) H-stable
--- H cyclic order p
--- M / N is free up to torsion rank r (as an ab group free rank r p)
--- r = r1 + r2 - 1 = NumberField.Units.rank
-
 
 section thm91
 variable
@@ -28,8 +23,6 @@ variable
 
 -- TODO maybe abbrev
 local notation3 "A" => CyclotomicIntegers p
-  -- MonoidAlgebra ℤ H ⧸ Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ H σ) ^ i}
-
 
 abbrev systemOfUnits.IsMaximal {r} {p : ℕ+} {G} [AddCommGroup G] [Module (CyclotomicIntegers p) G]
     (sys : systemOfUnits (G := G) p r) :=
@@ -85,7 +78,7 @@ lemma LinearIndependent.update {ι} [DecidableEq ι] {R} [CommRing R] [Module R
     · simp
     · simp
   ext j
-  have := FunLike.congr_fun (hf (Finsupp.update (σ • l) i (l i)) this) j
+  have := DFunLike.congr_fun (hf (Finsupp.update (σ • l) i (l i)) this) j
   simp only [Finsupp.coe_update, Finsupp.coe_smul, ne_eq, Function.update_apply, Finsupp.coe_zero,
     Pi.zero_apply] at this
   split_ifs at this with hij
@@ -123,7 +116,7 @@ lemma LinearIndependent.update' {ι} [DecidableEq ι] {R} [CommRing R] [Module R
   rw [smul_comm σ (l' i) g, hg, ← LinearMap.map_smul, ← LinearMap.map_smul, smul_smul,
     ← Finsupp.total_single, ← (Finsupp.total ι G R f).map_sub, ← map_add] at hl'
   replace hl' : ∀ j, (σ * l' j - (fun₀ | i => σ * l' i) j) + l' i * l j = 0 :=
-    fun j ↦ FunLike.congr_fun (hf _ hl') j
+    fun j ↦ DFunLike.congr_fun (hf _ hl') j
   simp only [Finsupp.single_apply] at hl'
   have : l' i = 0 := hl _ (by simpa using hl' i)
   simp only [this, zero_mul, add_zero, mul_zero, ite_self, sub_zero] at hl'
@@ -207,7 +200,7 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (i :
     letI : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
     rw [← LinearMap.map_smul, ← sub_eq_zero,
       ← (Finsupp.total (Fin _) G A S.units).map_sub] at hg
-    have := FunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i
+    have := DFunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i
     simp only [algebraMap_int_eq, Int.coe_castRingHom, Finsupp.coe_sub, Finsupp.coe_smul, ha,
       Pi.sub_apply, Finsupp.mapRange_apply, Finsupp.coe_zero, Pi.zero_apply, sub_eq_zero] at this
     exact CyclotomicIntegers.not_isUnit_one_sub_zeta p
@@ -276,7 +269,7 @@ noncomputable
 def relativeUnitsMapHom : (K →ₐ[k] K) →* (Monoid.End (RelativeUnits k K)) where
   toFun := relativeUnitsMap
   map_one' := by
-    refine FunLike.ext _ _ (fun x ↦ ?_)
+    refine DFunLike.ext _ _ (fun x ↦ ?_)
     obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
     rw [relativeUnitsMap]
     erw [QuotientGroup.lift_mk'] -- why?
@@ -285,7 +278,7 @@ def relativeUnitsMapHom : (K →ₐ[k] K) →* (Monoid.End (RelativeUnits k K))
     rfl
   map_mul' := by
     intros f g
-    refine FunLike.ext _ _ (fun x ↦ ?_)
+    refine DFunLike.ext _ _ (fun x ↦ ?_)
     obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
     simp only [relativeUnitsMap, map_mul, Monoid.coe_mul, Function.comp_apply]
     rfl
@@ -799,7 +792,7 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
 
 
 attribute [-instance] instDecidableEq Fintype.decidableForallFintype
-attribute [local instance 2000] MulHomClass.toFunLike Classical.propDecidable
+attribute [local instance 2000] MulHomClass.toDFunLike Classical.propDecidable
 
 lemma unit_to_U_pow (x) (n : ℕ) : mkG (x ^ n) = n • (mkG x) := by
   induction n with
@@ -822,7 +815,7 @@ lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by
   rw [← one_mul x, ← neg_mul, unit_to_U_mul, one_mul, add_left_eq_self]
   convert unit_to_U_map p hp hKL σ hσ (-1)
   ext
-  simp only [Units.val_neg, Units.val_one, AddSubgroupClass.coe_neg, OneMemClass.coe_one,
+  simp only [Units.val_neg, Units.val_one, OneMemClass.coe_one,
     Units.coe_map, MonoidHom.coe_coe, map_neg, map_one]
 
 instance : CommGroup (↥(𝓞 k))ˣ := inferInstance
@@ -852,8 +845,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
   have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ)
   · ext
     simp only [RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe,
-      RingOfInteger.coe_algebraMap_apply, RingOfIntegers.norm_apply_coe, Units.val_pow_eq_pow_val,
-      SubmonoidClass.coe_pow, Units.val_neg, AddSubgroupClass.coe_neg]
+      RingOfInteger.coe_algebraMap_apply, RingOfIntegers.norm_apply_coe, Units.val_pow_eq_pow_val, SubmonoidClass.coe_pow, Units.val_neg]
     rw [← map_pow] at hE
     refine Hilbert92ish_aux2 p hp hKL σ hσ E _ hE ?_ hpodd
     rw [← pow_mul, ← pow_succ']

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ca91956e8d5c311e00d6a69eb93d5eb5eef9b37d",
+   "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
+   "rev": "1c638703ed1c0c42aed2687acbeda67cec801454",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "241edd498be916e377e839d840ebee6ef3c706b0",
+   "rev": "e29e9b5cad835e581541cfb918245c72b6850245",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,