From fe4dd9a4b1c9d0abe9a58dcb5a8e928430089199 Mon Sep 17 00:00:00 2001
From: leanprover-community-bot <leanprover.community@gmail.com>
Date: Sun, 28 Jan 2024 06:39:32 +0000
Subject: [PATCH] bump to nightly-2024-01-28-06

mathlib commit https://github.com/leanprover-community/mathlib/commit/65a1391a0106c9204fe45bc73a039f056558cb83
---
 Mathbin/Data/Nat/Parity.lean         | 6 +++---
 Mathbin/RingTheory/Discriminant.lean | 2 +-
 lake-manifest.json                   | 8 ++++----
 lakefile.lean                        | 4 ++--
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Mathbin/Data/Nat/Parity.lean b/Mathbin/Data/Nat/Parity.lean
index 7657a5dee0..c82be26a5f 100644
--- a/Mathbin/Data/Nat/Parity.lean
+++ b/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 /-
diff --git a/Mathbin/RingTheory/Discriminant.lean b/Mathbin/RingTheory/Discriminant.lean
index cfbe5ea44b..dc943b72a7 100644
--- a/Mathbin/RingTheory/Discriminant.lean
+++ b/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
diff --git a/lake-manifest.json b/lake-manifest.json
index a9955ce765..363e49f72e 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/lakefile.lean b/lakefile.lean
index c3efcd7d8b..4c11445afa 100644
--- a/lakefile.lean
+++ b/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