bump to nightly-2024-01-28-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Data/Nat/Parity.lean

@@ -313,14 +313,14 @@ theorem even_mul_succ_self (n : ℕ) : Even (n * (n + 1)) :=
 #align nat.even_mul_succ_self Nat.even_mul_succ_self
 -/
 
-#print Nat.even_mul_self_pred /-
-theorem even_mul_self_pred (n : ℕ) : Even (n * (n - 1)) :=
+#print Nat.even_mul_pred_self /-
+theorem even_mul_pred_self (n : ℕ) : Even (n * (n - 1)) :=
   by
   cases n
   · exact even_zero
   · rw [mul_comm]
     apply even_mul_succ_self
-#align nat.even_mul_self_pred Nat.even_mul_self_pred
+#align nat.even_mul_self_pred Nat.even_mul_pred_self
 -/
 
 #print Nat.two_mul_div_two_of_even /-

Mathbin/RingTheory/Discriminant.lean

@@ -229,7 +229,7 @@ theorem discr_powerBasis_eq_prod'' [IsSeparable K L] (e : Fin pb.dim ≃ (L →
     by
     rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
     exact card_congr (Equiv.symm e)
-  have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := even_iff_two_dvd.1 (Nat.even_mul_self_pred _)
+  have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := even_iff_two_dvd.1 (Nat.even_mul_pred_self _)
   have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
   have hle : 1 ≤ pb.dim :=
     by

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "970a1ab2bfb8a7921fd05c872c630a0a83632bb8",
+   "rev": "62acecee993214f545acf44c171ee0e2a2fe4051",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "970a1ab2bfb8a7921fd05c872c630a0a83632bb8",
+   "inputRev": "62acecee993214f545acf44c171ee0e2a2fe4051",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "b1f6bf1e0388482dd12c4c9887d34e01aedb30f7",
+   "rev": "3b890e7719e32224564d4af64c69d2e725b421fb",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b1f6bf1e0388482dd12c4c9887d34e01aedb30f7",
+   "inputRev": "3b890e7719e32224564d4af64c69d2e725b421fb",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2024-01-27-06"
+def tag : String := "nightly-2024-01-28-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b1f6bf1e0388482dd12c4c9887d34e01aedb30f7"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3b890e7719e32224564d4af64c69d2e725b421fb"
 
 @[default_target]
 lean_lib Mathbin where