bump

Author: riccardobrasca

FltRegular/CaseI/Statement.lean

@@ -178,7 +178,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     contradiction
   obtain ⟨u, α, hu⟩ := is_principal hreg hp5 hgcd caseI H hζ
   rw [h, mul_comm _ (↑b : R), ← pow_one hζ'.unit'] at hu
-  obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' a b 1 hu.symm (by cutsat)
+  obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' a b 1 hu.symm (by lia)
   simp only [zpow_one, zpow_neg, mem_span_singleton, ← h] at hk
   have hpcoe : (p : ℤ) ≠ 0 := by simp [hpri.out.ne_zero]
   refine ⟨⟨(2 * k % p).natAbs, ?_⟩, ⟨((2 * k - 1) % p).natAbs, ?_⟩, ?_, ?_⟩

FltRegular/NumberTheory/Cyclotomic/CaseI.lean

@@ -47,7 +47,7 @@ theorem exists_int_sum_eq_zero'_aux (x y i : ℤ) [Fact (p.Prime)] (hp : 2 < p)
       map_units_inv] at H
     have h : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ := rfl
     simp [h, H]
-  refine (CommGroup.mem_torsion _ _).2 (isOfFinOrder_iff_pow_eq_one.2 ⟨p, by cutsat, ?_⟩)
+  refine (CommGroup.mem_torsion _ _).2 (isOfFinOrder_iff_pow_eq_one.2 ⟨p, by lia, ?_⟩)
   ext
   exact hζ.pow_eq_one
 

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -300,7 +300,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact p.Prime] {ζ : 𝓞 L}
   simp only [hlast, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
   rw [hζ.pow_sub_one_eq hp.out.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
     ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy
-  simp only [RelIso.coe_fn_toEquiv, Fin.coe_castSucc, Fin.coe_orderIso_apply] at hy
+  simp only [RelIso.coe_fn_toEquiv, Fin.val_castSucc, Fin.coe_orderIso_apply] at hy
   conv_lhs at hy =>
     congr; rfl; ext x
     rw [smul_neg]
@@ -346,7 +346,7 @@ theorem dvd_coeff_cycl_integer (hp : p.Prime) {ζ : 𝓞 L} (hζ : IsPrimitiveRo
   simp only [hlast, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
   rw [hζ.pow_sub_one_eq hp.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
     ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy
-  simp only [RelIso.coe_fn_toEquiv, Fin.coe_castSucc, Fin.coe_orderIso_apply] at hy
+  simp only [RelIso.coe_fn_toEquiv, Fin.val_castSucc, Fin.coe_orderIso_apply] at hy
   conv_lhs at hy =>
     congr; rfl; ext x
     rw [smul_neg]

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -259,7 +259,7 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (h
         RingOfIntegers.mapRingEquiv_apply, this, AlgEquiv.coe_ringEquiv, InvMemClass.coe_inv,
         map_units_inv] at H
       simp [H]
-    refine (CommGroup.mem_torsion _ _).2 (isOfFinOrder_iff_pow_eq_one.2 ⟨p, by cutsat, ?_⟩)
+    refine (CommGroup.mem_torsion _ _).2 (isOfFinOrder_iff_pow_eq_one.2 ⟨p, by lia, ?_⟩)
     ext
     exact hζ.pow_eq_one
   conv_lhs at hu' =>

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "77ef3eb515ad6bd125c596f0b164349d4a7d5bf5",
+   "rev": "05bb84181739ecc0897184a3e2906241267bcdfd",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
+   "rev": "63c92d89bf2723c770ea68f7f99885a44a302249",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
+   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "84b88f7ac9adf382b9668f852cee82487d616792",
+   "rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede",
+   "rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
+   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
+   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
+   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,17 +105,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
+   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.83",
+   "inputRev": "v0.0.84",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
+   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
+   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0-rc1