bump to nightly-2023-03-25-00

mathlib commit leanprover-community/mathlib@b19481d

Mathbin/Algebra/Order/Field/Power.lean

@@ -214,6 +214,12 @@ theorem zpow_two_nonneg (a : α) : 0 ≤ a ^ (2 : ℤ) :=
   zpow_bit0_nonneg _ _
 #align zpow_two_nonneg zpow_two_nonneg
 
+/- warning: zpow_neg_two_nonneg -> zpow_neg_two_nonneg is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : LinearOrderedField.{u1} α] (a : α), LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (OrderedAddCommGroup.toPartialOrder.{u1} α (StrictOrderedRing.toOrderedAddCommGroup.{u1} α (LinearOrderedRing.toStrictOrderedRing.{u1} α (LinearOrderedCommRing.toLinearOrderedRing.{u1} α (LinearOrderedField.toLinearOrderedCommRing.{u1} α _inst_1))))))) (OfNat.ofNat.{u1} α 0 (OfNat.mk.{u1} α 0 (Zero.zero.{u1} α (MulZeroClass.toHasZero.{u1} α (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} α (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} α (NonAssocRing.toNonUnitalNonAssocRing.{u1} α (Ring.toNonAssocRing.{u1} α (DivisionRing.toRing.{u1} α (Field.toDivisionRing.{u1} α (LinearOrderedField.toField.{u1} α _inst_1))))))))))) (HPow.hPow.{u1, 0, u1} α Int α (instHPow.{u1, 0} α Int (DivInvMonoid.Pow.{u1} α (DivisionRing.toDivInvMonoid.{u1} α (Field.toDivisionRing.{u1} α (LinearOrderedField.toField.{u1} α _inst_1))))) a (Neg.neg.{0} Int Int.hasNeg (OfNat.ofNat.{0} Int 2 (OfNat.mk.{0} Int 2 (bit0.{0} Int Int.hasAdd (One.one.{0} Int Int.hasOne))))))
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : LinearOrderedField.{u1} α] (a : α), LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (StrictOrderedRing.toPartialOrder.{u1} α (LinearOrderedRing.toStrictOrderedRing.{u1} α (LinearOrderedCommRing.toLinearOrderedRing.{u1} α (LinearOrderedField.toLinearOrderedCommRing.{u1} α _inst_1)))))) (OfNat.ofNat.{u1} α 0 (Zero.toOfNat0.{u1} α (CommMonoidWithZero.toZero.{u1} α (CommGroupWithZero.toCommMonoidWithZero.{u1} α (Semifield.toCommGroupWithZero.{u1} α (LinearOrderedSemifield.toSemifield.{u1} α (LinearOrderedField.toLinearOrderedSemifield.{u1} α _inst_1))))))) (HPow.hPow.{u1, 0, u1} α Int α (instHPow.{u1, 0} α Int (DivInvMonoid.Pow.{u1} α (DivisionRing.toDivInvMonoid.{u1} α (Field.toDivisionRing.{u1} α (LinearOrderedField.toField.{u1} α _inst_1))))) a (Neg.neg.{0} Int Int.instNegInt (OfNat.ofNat.{0} Int 2 (instOfNatInt 2))))
+Case conversion may be inaccurate. Consider using '#align zpow_neg_two_nonneg zpow_neg_two_nonnegₓ'. -/
 theorem zpow_neg_two_nonneg (a : α) : 0 ≤ a ^ (-2 : ℤ) :=
   zpow_bit0_nonneg _ (-1)
 #align zpow_neg_two_nonneg zpow_neg_two_nonneg

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "c0f227db827eeb683d27cd4bf1b818a03c51e4c0",
+    "rev": "7f557989d276edb798e56bfac9589f0091997e97",
     "name": "lean3port",
-    "inputRev?": "c0f227db827eeb683d27cd4bf1b818a03c51e4c0"}},
+    "inputRev?": "7f557989d276edb798e56bfac9589f0091997e97"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "31b48701ec27fb9ea5d144976b207fd69d9f618b",
+    "rev": "503db27e72224181ed1c7e8a7c1ba14c75c7280a",
     "name": "mathlib",
-    "inputRev?": "31b48701ec27fb9ea5d144976b207fd69d9f618b"}},
+    "inputRev?": "503db27e72224181ed1c7e8a7c1ba14c75c7280a"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-03-24-22"
+def tag : String := "nightly-2023-03-25-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c0f227db827eeb683d27cd4bf1b818a03c51e4c0"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"7f557989d276edb798e56bfac9589f0091997e97"
 
 @[default_target]
 lean_lib Mathbin where