bump to nightly-2023-05-08-12

mathlib commit leanprover-community/mathlib@08e1d8d

Mathbin/MeasureTheory/MeasurableSpace.lean

@@ -426,7 +426,7 @@ theorem measurable_of_subsingleton_codomain [Subsingleton β] (f : α → β) :
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : MeasurableSpace.{u1} α] [_inst_2 : MeasurableSpace.{u2} β] [_inst_4 : One.{u1} α], Measurable.{u2, u1} β α _inst_2 _inst_1 (OfNat.ofNat.{max u2 u1} (β -> α) 1 (OfNat.mk.{max u2 u1} (β -> α) 1 (One.one.{max u2 u1} (β -> α) (Pi.instOne.{u2, u1} β (fun (ᾰ : β) => α) (fun (i : β) => _inst_4)))))
 but is expected to have type
-  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : One.{u2} α], Measurable.{u1, u2} β α _inst_2 _inst_1 (OfNat.ofNat.{max u2 u1} (β -> α) 1 (One.toOfNat1.{max u2 u1} (β -> α) (Pi.instOne.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2070 : β) => α) (fun (i : β) => _inst_4))))
+  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : One.{u2} α], Measurable.{u1, u2} β α _inst_2 _inst_1 (OfNat.ofNat.{max u2 u1} (β -> α) 1 (One.toOfNat1.{max u2 u1} (β -> α) (Pi.instOne.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2073 : β) => α) (fun (i : β) => _inst_4))))
 Case conversion may be inaccurate. Consider using '#align measurable_one measurable_oneₓ'. -/
 @[to_additive]
 theorem measurable_one [One α] : Measurable (1 : β → α) :=
@@ -471,7 +471,7 @@ theorem measurable_const' {f : β → α} (hf : ∀ x y, f x = f y) : Measurable
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : MeasurableSpace.{u1} α] [_inst_2 : MeasurableSpace.{u2} β] [_inst_4 : NatCast.{u1} α] (n : Nat), Measurable.{u2, u1} β α _inst_2 _inst_1 ((fun (a : Type) (b : Sort.{max (succ u2) (succ u1)}) [self : HasLiftT.{1, max (succ u2) (succ u1)} a b] => self.0) Nat (β -> α) (HasLiftT.mk.{1, max (succ u2) (succ u1)} Nat (β -> α) (CoeTCₓ.coe.{1, max (succ u2) (succ u1)} Nat (β -> α) (Nat.castCoe.{max u2 u1} (β -> α) (Pi.hasNatCast.{u2, u1} β (fun (ᾰ : β) => α) (fun (a : β) => _inst_4))))) n)
 but is expected to have type
-  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : NatCast.{u2} α] (n : Nat), Measurable.{u1, u2} β α _inst_2 _inst_1 (Nat.cast.{max u2 u1} (β -> α) (Pi.natCast.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2315 : β) => α) (fun (a : β) => _inst_4)) n)
+  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : NatCast.{u2} α] (n : Nat), Measurable.{u1, u2} β α _inst_2 _inst_1 (Nat.cast.{max u2 u1} (β -> α) (Pi.natCast.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2319 : β) => α) (fun (a : β) => _inst_4)) n)
 Case conversion may be inaccurate. Consider using '#align measurable_nat_cast measurable_natCastₓ'. -/
 @[measurability]
 theorem measurable_natCast [NatCast α] (n : ℕ) : Measurable (n : β → α) :=
@@ -482,7 +482,7 @@ theorem measurable_natCast [NatCast α] (n : ℕ) : Measurable (n : β → α) :
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : MeasurableSpace.{u1} α] [_inst_2 : MeasurableSpace.{u2} β] [_inst_4 : IntCast.{u1} α] (n : Int), Measurable.{u2, u1} β α _inst_2 _inst_1 ((fun (a : Type) (b : Sort.{max (succ u2) (succ u1)}) [self : HasLiftT.{1, max (succ u2) (succ u1)} a b] => self.0) Int (β -> α) (HasLiftT.mk.{1, max (succ u2) (succ u1)} Int (β -> α) (CoeTCₓ.coe.{1, max (succ u2) (succ u1)} Int (β -> α) (Int.castCoe.{max u2 u1} (β -> α) (Pi.hasIntCast.{u2, u1} β (fun (ᾰ : β) => α) (fun (i : β) => _inst_4))))) n)
 but is expected to have type
-  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : IntCast.{u2} α] (n : Int), Measurable.{u1, u2} β α _inst_2 _inst_1 (Int.cast.{max u2 u1} (β -> α) (Pi.intCast.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2364 : β) => α) (fun (i : β) => _inst_4)) n)
+  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : MeasurableSpace.{u1} β] [_inst_4 : IntCast.{u2} α] (n : Int), Measurable.{u1, u2} β α _inst_2 _inst_1 (Int.cast.{max u2 u1} (β -> α) (Pi.intCast.{u1, u2} β (fun (a._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.2369 : β) => α) (fun (i : β) => _inst_4)) n)
 Case conversion may be inaccurate. Consider using '#align measurable_int_cast measurable_intCastₓ'. -/
 @[measurability]
 theorem measurable_intCast [IntCast α] (n : ℤ) : Measurable (n : β → α) :=
@@ -2505,7 +2505,7 @@ def piEquivPiSubtypeProd (p : δ' → Prop) [DecidablePred p] :
 lean 3 declaration is
   forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {s : Set.{u1} α} [_inst_7 : DecidablePred.{succ u1} α s], (MeasurableSet.{u1} α _inst_1 s) -> (MeasurableEquiv.{u1, u1} (Sum.{u1, u1} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.booleanAlgebra.{u1} α)) s))) α (Sum.measurableSpace.{u1, u1} (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) s) (coeSort.{succ u1, succ (succ u1)} (Set.{u1} α) Type.{u1} (Set.hasCoeToSort.{u1} α) (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.booleanAlgebra.{u1} α)) s)) (Subtype.measurableSpace.{u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x s) _inst_1) (Subtype.measurableSpace.{u1} α (fun (x : α) => Membership.Mem.{u1, u1} α (Set.{u1} α) (Set.hasMem.{u1} α) x (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.booleanAlgebra.{u1} α)) s)) _inst_1)) _inst_1)
 but is expected to have type
-  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {s : Set.{u1} α} [_inst_7 : DecidablePred.{succ u1} α (fun (x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17266 : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17266 s)], (MeasurableSet.{u1} α _inst_1 s) -> (MeasurableEquiv.{u1, u1} (Sum.{u1, u1} (Set.Elem.{u1} α s) (Set.Elem.{u1} α (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s))) α (instMeasurableSpaceSum.{u1, u1} (Set.Elem.{u1} α s) (Set.Elem.{u1} α (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s)) (instMeasurableSpaceSubtype.{u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x s) _inst_1) (instMeasurableSpaceSubtype.{u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s)) _inst_1)) _inst_1)
+  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {s : Set.{u1} α} [_inst_7 : DecidablePred.{succ u1} α (fun (x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17302 : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17302 s)], (MeasurableSet.{u1} α _inst_1 s) -> (MeasurableEquiv.{u1, u1} (Sum.{u1, u1} (Set.Elem.{u1} α s) (Set.Elem.{u1} α (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s))) α (instMeasurableSpaceSum.{u1, u1} (Set.Elem.{u1} α s) (Set.Elem.{u1} α (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s)) (instMeasurableSpaceSubtype.{u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x s) _inst_1) (instMeasurableSpaceSubtype.{u1} α (fun (x : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x (HasCompl.compl.{u1} (Set.{u1} α) (BooleanAlgebra.toHasCompl.{u1} (Set.{u1} α) (Set.instBooleanAlgebraSet.{u1} α)) s)) _inst_1)) _inst_1)
 Case conversion may be inaccurate. Consider using '#align measurable_equiv.sum_compl MeasurableEquiv.sumComplₓ'. -/
 /-- If `s` is a measurable set in a measurable space, that space is equivalent
 to the sum of `s` and `sᶜ`.-/

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "9c2c2926f3032f8e0cd26e83c013b73704855fb6",
+    "rev": "e79655e0ec7f70ad3ad163e5f317946865138ebb",
     "name": "lean3port",
-    "inputRev?": "9c2c2926f3032f8e0cd26e83c013b73704855fb6"}},
+    "inputRev?": "e79655e0ec7f70ad3ad163e5f317946865138ebb"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "4c90d545f68261230bec80537e66728fbe749744",
+    "rev": "3d31c9ec03783d96b3230b05ec8625c8fb63758f",
     "name": "mathlib",
-    "inputRev?": "4c90d545f68261230bec80537e66728fbe749744"}},
+    "inputRev?": "3d31c9ec03783d96b3230b05ec8625c8fb63758f"}},
   {"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-08-10"
+def tag : String := "nightly-2023-05-08-12"
 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"@"9c2c2926f3032f8e0cd26e83c013b73704855fb6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e79655e0ec7f70ad3ad163e5f317946865138ebb"
 
 @[default_target]
 lean_lib Mathbin where