bump to nightly-2023-05-11-22

mathlib commit leanprover-community/mathlib@28b2a92

Mathbin/Algebra/Group/Basic.lean

@@ -1451,6 +1451,12 @@ theorem mul_div_cancel'' (a b : G) : a * b / b = a := by
 #align mul_div_cancel'' mul_div_cancel''
 #align add_sub_cancel add_sub_cancel
 
+/- warning: div_mul_cancel''' -> div_mul_cancel''' is a dubious translation:
+lean 3 declaration is
+  forall {G : Type.{u1}} [_inst_1 : Group.{u1} G] (a : G) (b : G), Eq.{succ u1} G (HDiv.hDiv.{u1, u1, u1} G G G (instHDiv.{u1} G (DivInvMonoid.toHasDiv.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1))) a (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1))))) b a)) (Inv.inv.{u1} G (DivInvMonoid.toHasInv.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1)) b)
+but is expected to have type
+  forall {G : Type.{u1}} [_inst_1 : Group.{u1} G] (a : G) (b : G), Eq.{succ u1} G (HDiv.hDiv.{u1, u1, u1} G G G (instHDiv.{u1} G (DivInvMonoid.toDiv.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1))) a (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_1))))) b a)) (Inv.inv.{u1} G (InvOneClass.toInv.{u1} G (DivInvOneMonoid.toInvOneClass.{u1} G (DivisionMonoid.toDivInvOneMonoid.{u1} G (Group.toDivisionMonoid.{u1} G _inst_1)))) b)
+Case conversion may be inaccurate. Consider using '#align div_mul_cancel''' div_mul_cancel'''ₓ'. -/
 @[simp, to_additive sub_add_cancel'']
 theorem div_mul_cancel''' (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel'']
 #align div_mul_cancel''' div_mul_cancel'''

Mathbin/Algebra/GroupPower/Lemmas.lean

@@ -867,6 +867,12 @@ theorem mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n)
   rw [mul_add, mul_bit0, mul_one]
 #align mul_bit1 mul_bit1
 
+/- warning: int.cast_mul_eq_zsmul_cast -> Int.cast_mul_eq_zsmul_cast is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : AddCommGroupWithOne.{u1} α] (m : Int) (n : Int), Eq.{succ u1} α ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int α (HasLiftT.mk.{1, succ u1} Int α (CoeTCₓ.coe.{1, succ u1} Int α (Int.castCoe.{u1} α (AddGroupWithOne.toHasIntCast.{u1} α (AddCommGroupWithOne.toAddGroupWithOne.{u1} α _inst_1))))) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.hasMul) m n)) (SMul.smul.{0, u1} Int α (SubNegMonoid.SMulInt.{u1} α (AddGroup.toSubNegMonoid.{u1} α (AddGroupWithOne.toAddGroup.{u1} α (AddCommGroupWithOne.toAddGroupWithOne.{u1} α _inst_1)))) m ((fun (a : Type) (b : Type.{u1}) [self : HasLiftT.{1, succ u1} a b] => self.0) Int α (HasLiftT.mk.{1, succ u1} Int α (CoeTCₓ.coe.{1, succ u1} Int α (Int.castCoe.{u1} α (AddGroupWithOne.toHasIntCast.{u1} α (AddCommGroupWithOne.toAddGroupWithOne.{u1} α _inst_1))))) n))
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : AddCommGroupWithOne.{u1} α] (m : Int) (n : Int), Eq.{succ u1} α (Int.cast.{u1} α (AddCommGroupWithOne.toIntCast.{u1} α _inst_1) (HMul.hMul.{0, 0, 0} Int Int Int (instHMul.{0} Int Int.instMulInt) m n)) (Int.cast.{u1} α (AddCommGroupWithOne.toIntCast.{u1} α _inst_1) (HSMul.hSMul.{0, 0, 0} Int Int Int (instHSMul.{0, 0} Int Int (SubNegMonoid.SMulInt.{0} Int (AddGroup.toSubNegMonoid.{0} Int Int.instAddGroupInt))) m n))
+Case conversion may be inaccurate. Consider using '#align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_castₓ'. -/
 /-- Note this holds in marginally more generality than `int.cast_mul` -/
 theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] : ∀ m n, ((m * n : ℤ) : α) = m • n :=
   fun m =>
@@ -1218,7 +1224,7 @@ alias le_self_sq ← le_self_pow_two
 lean 3 declaration is
   forall {x : Int}, (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) (Int.natAbs x)) -> (Function.Injective.{1, 1} Nat Int (HPow.hPow.{0, 0, 0} Int Nat Int (instHPow.{0, 0} Int Nat (Monoid.Pow.{0} Int Int.monoid)) x))
 but is expected to have type
-  forall {x : Int}, (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (Int.natAbs x)) -> (Function.Injective.{1, 1} Nat Int ((fun (x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8024 : Int) (x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8026 : Nat) => HPow.hPow.{0, 0, 0} Int Nat Int Int.instHPowIntNat x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8024 x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8026) x))
+  forall {x : Int}, (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (Int.natAbs x)) -> (Function.Injective.{1, 1} Nat Int ((fun (x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8104 : Int) (x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8106 : Nat) => HPow.hPow.{0, 0, 0} Int Nat Int Int.instHPowIntNat x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8104 x._@.Mathlib.Algebra.GroupPower.Lemmas._hyg.8106) x))
 Case conversion may be inaccurate. Consider using '#align int.pow_right_injective Int.pow_right_injectiveₓ'. -/
 theorem pow_right_injective {x : ℤ} (h : 1 < x.natAbs) : Function.Injective ((· ^ ·) x : ℕ → ℤ) :=
   by

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "a000bb510ea2892017461a458fd6507bd5e1d4de",
+    "rev": "229c5b50fb0238e7633979f9f470177e7780d10f",
     "name": "lean3port",
-    "inputRev?": "a000bb510ea2892017461a458fd6507bd5e1d4de"}},
+    "inputRev?": "229c5b50fb0238e7633979f9f470177e7780d10f"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "791d8ddd8d472b4909de913bc0b2733d1ecb0b85",
+    "rev": "e122338e0d96df2d5bee21a2d76d69157923b325",
     "name": "mathlib",
-    "inputRev?": "791d8ddd8d472b4909de913bc0b2733d1ecb0b85"}},
+    "inputRev?": "e122338e0d96df2d5bee21a2d76d69157923b325"}},
   {"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-05-11-20"
+def tag : String := "nightly-2023-05-11-22"
 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"@"a000bb510ea2892017461a458fd6507bd5e1d4de"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"229c5b50fb0238e7633979f9f470177e7780d10f"
 
 @[default_target]
 lean_lib Mathbin where