bump to nightly-2023-09-04-06

mathlib commit leanprover-community/mathlib@442a83d
leanprover-community · Sep 4, 2023 · 9fbca49 · 9fbca49
1 parent 9ddbe05
commit 9fbca49
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/Mathbin/GroupTheory/GroupAction/Basic.lean b/Mathbin/GroupTheory/GroupAction/Basic.lean
@@ -231,7 +231,7 @@ theorem mem_fixedPoints_iff_card_orbit_eq_one {a : β} [Fintype (orbit α a)] :
       x • a = z := Subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
       _ = a := (Subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm
 #align mul_action.mem_fixed_points_iff_card_orbit_eq_one MulAction.mem_fixedPoints_iff_card_orbit_eq_one
-#align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_zero
+#align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_one
 -/
 
 end MulAction

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -12,10 +12,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "03e9ea44411712c1f389a43430f7328b930a7710",
+    "rev": "f5c736c5a02cf768b3db7b2cad5a122794246968",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "03e9ea44411712c1f389a43430f7328b930a7710",
+    "inputRev?": "f5c736c5a02cf768b3db7b2cad5a122794246968",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -28,10 +28,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ab6dac98bb953d089da09ebad00a2ec2b39794ce",
+    "rev": "acc7084b6ebbdb1f2f27776bf26acc1ef9b829fb",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "ab6dac98bb953d089da09ebad00a2ec2b39794ce",
+    "inputRev?": "acc7084b6ebbdb1f2f27776bf26acc1ef9b829fb",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

diff --git 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-2023-09-03-06"
+def tag : String := "nightly-2023-09-04-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"@"03e9ea44411712c1f389a43430f7328b930a7710"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f5c736c5a02cf768b3db7b2cad5a122794246968"
 
 @[default_target]
 lean_lib Mathbin where