bump to nightly-2023-03-28-22

mathlib commit leanprover-community/mathlib@728baa2

Mathbin/Algebra/Star/SelfAdjoint.lean

@@ -123,7 +123,7 @@ theorem mul_star_self [Semigroup R] [StarSemigroup R] (x : R) : IsSelfAdjoint (x
 lean 3 declaration is
   forall {F : Type.{u1}} {R : Type.{u2}} {S : Type.{u3}} [_inst_1 : Star.{u2} R] [_inst_2 : Star.{u3} S] [_inst_3 : StarHomClass.{u1, u2, u3} F R S _inst_1 _inst_2] {x : R}, (IsSelfAdjoint.{u2} R _inst_1 x) -> (forall (f : F), IsSelfAdjoint.{u3} S _inst_2 (coeFn.{succ u1, max (succ u2) (succ u3)} F (fun (_x : F) => R -> S) (FunLike.hasCoeToFun.{succ u1, succ u2, succ u3} F R (fun (_x : R) => S) (StarHomClass.toFunLike.{u1, u2, u3} F R S _inst_1 _inst_2 _inst_3)) f x))
 but is expected to have type
-  forall {F : Type.{u3}} {R : Type.{u2}} {S : Type.{u1}} [_inst_1 : Star.{u2} R] [_inst_2 : Star.{u1} S] [_inst_3 : StarHomClass.{u3, u2, u1} F R S _inst_1 _inst_2] {x : R}, (IsSelfAdjoint.{u2} R _inst_1 x) -> (forall (f : F), IsSelfAdjoint.{u1} ((fun (x._@.Mathlib.Algebra.Star.Basic._hyg.3024 : R) => S) x) _inst_2 (FunLike.coe.{succ u3, succ u2, succ u1} F R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Star.Basic._hyg.3024 : R) => S) _x) (StarHomClass.toFunLike.{u3, u2, u1} F R S _inst_1 _inst_2 _inst_3) f x))
+  forall {F : Type.{u3}} {R : Type.{u2}} {S : Type.{u1}} [_inst_1 : Star.{u2} R] [_inst_2 : Star.{u1} S] [_inst_3 : StarHomClass.{u3, u2, u1} F R S _inst_1 _inst_2] {x : R}, (IsSelfAdjoint.{u2} R _inst_1 x) -> (forall (f : F), IsSelfAdjoint.{u1} ((fun (x._@.Mathlib.Algebra.Star.Basic._hyg.3050 : R) => S) x) _inst_2 (FunLike.coe.{succ u3, succ u2, succ u1} F R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Star.Basic._hyg.3050 : R) => S) _x) (StarHomClass.toFunLike.{u3, u2, u1} F R S _inst_1 _inst_2 _inst_3) f x))
 Case conversion may be inaccurate. Consider using '#align is_self_adjoint.star_hom_apply IsSelfAdjoint.starHom_applyₓ'. -/
 /-- Functions in a `star_hom_class` preserve self-adjoint elements. -/
 theorem starHom_apply {F R S : Type _} [Star R] [Star S] [StarHomClass F R S] {x : R}

Mathbin/Data/Nat/Cast/Basic.lean

@@ -483,7 +483,7 @@ end Pi
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} {γ : Type.{u3}} [_inst_1 : NatCast.{u3} γ] (n : Nat), Eq.{max (max (succ u1) (succ u2)) (succ u3)} ((Sum.{u1, u2} α β) -> γ) (Sum.elim.{u1, u2, succ u3} α β γ ((fun (a : Type) (b : Sort.{max (succ u1) (succ u3)}) [self : HasLiftT.{1, max (succ u1) (succ u3)} a b] => self.0) Nat (α -> γ) (HasLiftT.mk.{1, max (succ u1) (succ u3)} Nat (α -> γ) (CoeTCₓ.coe.{1, max (succ u1) (succ u3)} Nat (α -> γ) (Nat.castCoe.{max u1 u3} (α -> γ) (Pi.hasNatCast.{u1, u3} α (fun (ᾰ : α) => γ) (fun (a : α) => _inst_1))))) n) ((fun (a : Type) (b : Sort.{max (succ u2) (succ u3)}) [self : HasLiftT.{1, max (succ u2) (succ u3)} a b] => self.0) Nat (β -> γ) (HasLiftT.mk.{1, max (succ u2) (succ u3)} Nat (β -> γ) (CoeTCₓ.coe.{1, max (succ u2) (succ u3)} Nat (β -> γ) (Nat.castCoe.{max u2 u3} (β -> γ) (Pi.hasNatCast.{u2, u3} β (fun (ᾰ : β) => γ) (fun (a : β) => _inst_1))))) n)) ((fun (a : Type) (b : Sort.{max (max (succ u1) (succ u2)) (succ u3)}) [self : HasLiftT.{1, max (max (succ u1) (succ u2)) (succ u3)} a b] => self.0) Nat ((Sum.{u1, u2} α β) -> γ) (HasLiftT.mk.{1, max (max (succ u1) (succ u2)) (succ u3)} Nat ((Sum.{u1, u2} α β) -> γ) (CoeTCₓ.coe.{1, max (max (succ u1) (succ u2)) (succ u3)} Nat ((Sum.{u1, u2} α β) -> γ) (Nat.castCoe.{max (max u1 u2) u3} ((Sum.{u1, u2} α β) -> γ) (Pi.hasNatCast.{max u1 u2, u3} (Sum.{u1, u2} α β) (fun (ᾰ : Sum.{u1, u2} α β) => γ) (fun (a : Sum.{u1, u2} α β) => _inst_1))))) n)
 but is expected to have type
-  forall {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : NatCast.{u1} γ] (n : Nat), Eq.{max (max (succ u3) (succ u2)) (succ u1)} ((Sum.{u3, u2} α β) -> γ) (Sum.elim.{u3, u2, succ u1} α β γ (Nat.cast.{max u3 u1} (α -> γ) (Pi.natCast.{u3, u1} α (fun (a._@.Mathlib.Data.Nat.Cast.Basic._hyg.2224 : α) => γ) (fun (a : α) => _inst_1)) n) (Nat.cast.{max u2 u1} (β -> γ) (Pi.natCast.{u2, u1} β (fun (a._@.Mathlib.Data.Nat.Cast.Basic._hyg.2231 : β) => γ) (fun (a : β) => _inst_1)) n)) (Nat.cast.{max (max u3 u2) u1} ((Sum.{u3, u2} α β) -> γ) (Pi.natCast.{max u3 u2, u1} (Sum.{u3, u2} α β) (fun (a._@.Mathlib.Data.Sum.Basic._hyg.1871 : Sum.{u3, u2} α β) => γ) (fun (a : Sum.{u3, u2} α β) => _inst_1)) n)
+  forall {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : NatCast.{u1} γ] (n : Nat), Eq.{max (max (succ u3) (succ u2)) (succ u1)} ((Sum.{u3, u2} α β) -> γ) (Sum.elim.{u3, u2, succ u1} α β γ (Nat.cast.{max u3 u1} (α -> γ) (Pi.natCast.{u3, u1} α (fun (a._@.Mathlib.Data.Nat.Cast.Basic._hyg.2266 : α) => γ) (fun (a : α) => _inst_1)) n) (Nat.cast.{max u2 u1} (β -> γ) (Pi.natCast.{u2, u1} β (fun (a._@.Mathlib.Data.Nat.Cast.Basic._hyg.2273 : β) => γ) (fun (a : β) => _inst_1)) n)) (Nat.cast.{max (max u3 u2) u1} ((Sum.{u3, u2} α β) -> γ) (Pi.natCast.{max u3 u2, u1} (Sum.{u3, u2} α β) (fun (a._@.Mathlib.Data.Sum.Basic._hyg.1871 : Sum.{u3, u2} α β) => γ) (fun (a : Sum.{u3, u2} α β) => _inst_1)) n)
 Case conversion may be inaccurate. Consider using '#align sum.elim_nat_cast_nat_cast Sum.elim_natCast_natCastₓ'. -/
 theorem Sum.elim_natCast_natCast {α β γ : Type _} [NatCast γ] (n : ℕ) :
     Sum.elim (n : α → γ) (n : β → γ) = n :=

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "35a157f2d75cd3e473d74a364509c57784d3e1e4",
+    "rev": "1e011598daa33cdaa99cd6ef55e0ff2b852f2fb9",
     "name": "lean3port",
-    "inputRev?": "35a157f2d75cd3e473d74a364509c57784d3e1e4"}},
+    "inputRev?": "1e011598daa33cdaa99cd6ef55e0ff2b852f2fb9"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ad723d1303fede81b66d564ba70cd79b3e3f7b9a",
+    "rev": "02c081e80e62f203e6962de6adce430cf9b70871",
     "name": "mathlib",
-    "inputRev?": "ad723d1303fede81b66d564ba70cd79b3e3f7b9a"}},
+    "inputRev?": "02c081e80e62f203e6962de6adce430cf9b70871"}},
   {"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-28-20"
+def tag : String := "nightly-2023-03-28-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"@"35a157f2d75cd3e473d74a364509c57784d3e1e4"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"1e011598daa33cdaa99cd6ef55e0ff2b852f2fb9"
 
 @[default_target]
 lean_lib Mathbin where