bump to nightly-2023-04-28-00

mathlib commit leanprover-community/mathlib@9b2b58d

Mathbin/CategoryTheory/Noetherian.lean

@@ -34,6 +34,7 @@ open CategoryTheory.Limits
 
 variable {C : Type _} [Category C]
 
+#print CategoryTheory.NoetherianObject /-
 /-- A noetherian object is an object
 which does not have infinite increasing sequences of subobjects.
 
@@ -42,7 +43,9 @@ See https://stacks.math.columbia.edu/tag/0FCG
 class NoetherianObject (X : C) : Prop where
   subobject_gt_wellFounded : WellFounded ((· > ·) : Subobject X → Subobject X → Prop)
 #align category_theory.noetherian_object CategoryTheory.NoetherianObject
+-/
 
+#print CategoryTheory.ArtinianObject /-
 /- ./././Mathport/Syntax/Translate/Command.lean:393:30: infer kinds are unsupported in Lean 4: #[`subobject_lt_wellFounded] [] -/
 /-- An artinian object is an object
 which does not have infinite decreasing sequences of subobjects.
@@ -52,20 +55,25 @@ See https://stacks.math.columbia.edu/tag/0FCF
 class ArtinianObject (X : C) : Prop where
   subobject_lt_wellFounded : WellFounded ((· < ·) : Subobject X → Subobject X → Prop)
 #align category_theory.artinian_object CategoryTheory.ArtinianObject
+-/
 
 variable (C)
 
+#print CategoryTheory.Noetherian /-
 /-- A category is noetherian if it is essentially small and all objects are noetherian. -/
 class Noetherian extends EssentiallySmall C where
   NoetherianObject : ∀ X : C, NoetherianObject X
 #align category_theory.noetherian CategoryTheory.Noetherian
+-/
 
 attribute [instance] noetherian.noetherian_object
 
+#print CategoryTheory.Artinian /-
 /-- A category is artinian if it is essentially small and all objects are artinian. -/
 class Artinian extends EssentiallySmall C where
   ArtinianObject : ∀ X : C, ArtinianObject X
 #align category_theory.artinian CategoryTheory.Artinian
+-/
 
 attribute [instance] artinian.artinian_object
 
@@ -75,6 +83,12 @@ open Subobject
 
 variable [HasZeroMorphisms C] [HasZeroObject C]
 
+/- warning: category_theory.exists_simple_subobject -> CategoryTheory.exists_simple_subobject is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u1}} [_inst_1 : CategoryTheory.Category.{u2, u1} C] [_inst_2 : CategoryTheory.Limits.HasZeroMorphisms.{u2, u1} C _inst_1] [_inst_3 : CategoryTheory.Limits.HasZeroObject.{u2, u1} C _inst_1] {X : C} [_inst_4 : CategoryTheory.ArtinianObject.{u1, u2} C _inst_1 X], (Not (CategoryTheory.Limits.IsZero.{u2, u1} C _inst_1 X)) -> (Exists.{succ (max u1 u2)} (CategoryTheory.Subobject.{u2, u1} C _inst_1 X) (fun (Y : CategoryTheory.Subobject.{u2, u1} C _inst_1 X) => CategoryTheory.Simple.{u2, u1} C _inst_1 _inst_2 ((fun (a : Type.{max u1 u2}) (b : Type.{u1}) [self : HasLiftT.{succ (max u1 u2), succ u1} a b] => self.0) (CategoryTheory.Subobject.{u2, u1} C _inst_1 X) C (HasLiftT.mk.{succ (max u1 u2), succ u1} (CategoryTheory.Subobject.{u2, u1} C _inst_1 X) C (CoeTCₓ.coe.{succ (max u1 u2), succ u1} (CategoryTheory.Subobject.{u2, u1} C _inst_1 X) C (coeBase.{succ (max u1 u2), succ u1} (CategoryTheory.Subobject.{u2, u1} C _inst_1 X) C (CategoryTheory.Subobject.hasCoe.{u2, u1} C _inst_1 X)))) Y)))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Limits.HasZeroMorphisms.{u1, u2} C _inst_1] [_inst_3 : CategoryTheory.Limits.HasZeroObject.{u1, u2} C _inst_1] {X : C} [_inst_4 : CategoryTheory.ArtinianObject.{u2, u1} C _inst_1 X], (Not (CategoryTheory.Limits.IsZero.{u1, u2} C _inst_1 X)) -> (Exists.{max (succ u2) (succ u1)} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (fun (Y : CategoryTheory.Subobject.{u1, u2} C _inst_1 X) => CategoryTheory.Simple.{u1, u2} C _inst_1 _inst_2 (Prefunctor.obj.{max (succ u2) (succ u1), succ u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 X))))) C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) (CategoryTheory.Functor.toPrefunctor.{max u2 u1, u1, max u2 u1, u2} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (Preorder.smallCategory.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (PartialOrder.toPreorder.{max u2 u1} (CategoryTheory.Subobject.{u1, u2} C _inst_1 X) (CategoryTheory.instPartialOrderSubobject.{u1, u2} C _inst_1 X))) C _inst_1 (CategoryTheory.Subobject.underlying.{u1, u2} C _inst_1 X)) Y)))
+Case conversion may be inaccurate. Consider using '#align category_theory.exists_simple_subobject CategoryTheory.exists_simple_subobjectₓ'. -/
 theorem exists_simple_subobject {X : C} [ArtinianObject X] (h : ¬IsZero X) :
     ∃ Y : Subobject X, Simple (Y : C) :=
   by
@@ -85,16 +99,20 @@ theorem exists_simple_subobject {X : C} [ArtinianObject X] (h : ¬IsZero X) :
   exact ⟨Y, (subobject_simple_iff_is_atom _).mpr s.1⟩
 #align category_theory.exists_simple_subobject CategoryTheory.exists_simple_subobject
 
+#print CategoryTheory.simpleSubobject /-
 /-- Choose an arbitrary simple subobject of a non-zero artinian object. -/
 noncomputable def simpleSubobject {X : C} [ArtinianObject X] (h : ¬IsZero X) : C :=
   (exists_simple_subobject h).some
 #align category_theory.simple_subobject CategoryTheory.simpleSubobject
+-/
 
+#print CategoryTheory.simpleSubobjectArrow /-
 /-- The monomorphism from the arbitrary simple subobject of a non-zero artinian object. -/
 noncomputable def simpleSubobjectArrow {X : C} [ArtinianObject X] (h : ¬IsZero X) :
     simpleSubobject h ⟶ X :=
   (exists_simple_subobject h).some.arrow deriving Mono
 #align category_theory.simple_subobject_arrow CategoryTheory.simpleSubobjectArrow
+-/
 
 instance {X : C} [ArtinianObject X] (h : ¬IsZero X) : Simple (simpleSubobject h) :=
   (exists_simple_subobject h).choose_spec

Mathbin/MeasureTheory/MeasurableSpace.lean

@@ -665,6 +665,12 @@ theorem measurable_to_countable [MeasurableSpace α] [Countable α] [MeasurableS
   · simp only [preimage_singleton_eq_empty.2 hyf, MeasurableSet.empty]
 #align measurable_to_countable measurable_to_countable
 
+/- warning: measurable_to_countable' -> measurable_to_countable' is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : MeasurableSpace.{u1} α] [_inst_2 : Countable.{succ u1} α] [_inst_3 : MeasurableSpace.{u2} β] {f : β -> α}, (forall (x : α), MeasurableSet.{u2} β _inst_3 (Set.preimage.{u2, u1} β α f (Singleton.singleton.{u1, u1} α (Set.{u1} α) (Set.hasSingleton.{u1} α) x))) -> (Measurable.{u2, u1} β α _inst_3 _inst_1 f)
+but is expected to have type
+  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : MeasurableSpace.{u2} α] [_inst_2 : Countable.{succ u2} α] [_inst_3 : MeasurableSpace.{u1} β] {f : β -> α}, (forall (x : α), MeasurableSet.{u1} β _inst_3 (Set.preimage.{u1, u2} β α f (Singleton.singleton.{u2, u2} α (Set.{u2} α) (Set.instSingletonSet.{u2} α) x))) -> (Measurable.{u1, u2} β α _inst_3 _inst_1 f)
+Case conversion may be inaccurate. Consider using '#align measurable_to_countable' measurable_to_countable'ₓ'. -/
 theorem measurable_to_countable' [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α}
     (h : ∀ x, MeasurableSet (f ⁻¹' {x})) : Measurable f :=
   measurable_to_countable fun y => h (f y)
@@ -706,6 +712,12 @@ theorem measurable_to_nat {f : α → ℕ} : (∀ y, MeasurableSet (f ⁻¹' {f
   measurable_to_countable
 #align measurable_to_nat measurable_to_nat
 
+/- warning: measurable_to_bool -> measurable_to_bool is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {f : α -> Bool}, (MeasurableSet.{u1} α _inst_1 (Set.preimage.{u1, 0} α Bool f (Singleton.singleton.{0, 0} Bool (Set.{0} Bool) (Set.hasSingleton.{0} Bool) Bool.true))) -> (Measurable.{u1, 0} α Bool _inst_1 Bool.measurableSpace f)
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : MeasurableSpace.{u1} α] {f : α -> Bool}, (MeasurableSet.{u1} α _inst_1 (Set.preimage.{u1, 0} α Bool f (Singleton.singleton.{0, 0} Bool (Set.{0} Bool) (Set.instSingletonSet.{0} Bool) Bool.true))) -> (Measurable.{u1, 0} α Bool _inst_1 instMeasurableSpaceBool f)
+Case conversion may be inaccurate. Consider using '#align measurable_to_bool measurable_to_boolₓ'. -/
 theorem measurable_to_bool {f : α → Bool} (h : MeasurableSet (f ⁻¹' {true})) : Measurable f :=
   by
   apply measurable_to_countable'
@@ -2493,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.17087 : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17087 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.17268 : α) => Membership.mem.{u1, u1} α (Set.{u1} α) (Set.instMembershipSet.{u1} α) x._@.Mathlib.MeasureTheory.MeasurableSpace._hyg.17268 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ᶜ`.-/
@@ -2624,14 +2636,22 @@ namespace MeasurableSpace
 
 variable (α)
 
+#print MeasurableSpace.CountablyGenerated /-
 /-- We say a measurable space is countably generated
 if can be generated by a countable set of sets.-/
 class CountablyGenerated [m : MeasurableSpace α] : Prop where
   IsCountablyGenerated : ∃ b : Set (Set α), b.Countable ∧ m = generateFrom b
 #align measurable_space.countably_generated MeasurableSpace.CountablyGenerated
+-/
 
 open Classical
 
+/- warning: measurable_space.measurable_injection_cantor_of_countably_generated -> MeasurableSpace.measurable_injection_cantor_of_countablyGenerated is a dubious translation:
+lean 3 declaration is
+  forall (α : Type.{u1}) [_inst_1 : MeasurableSpace.{u1} α] [h : MeasurableSpace.CountablyGenerated.{u1} α _inst_1] [_inst_2 : MeasurableSingletonClass.{u1} α _inst_1], Exists.{succ u1} (α -> Nat -> Bool) (fun (f : α -> Nat -> Bool) => And (Measurable.{u1, 0} α (Nat -> Bool) _inst_1 (MeasurableSpace.pi.{0, 0} Nat (fun (ᾰ : Nat) => Bool) (fun (a : Nat) => Bool.measurableSpace)) f) (Function.Injective.{succ u1, 1} α (Nat -> Bool) f))
+but is expected to have type
+  forall (α : Type.{u1}) [_inst_1 : MeasurableSpace.{u1} α] [h : MeasurableSpace.CountablyGenerated.{u1} α _inst_1] [_inst_2 : MeasurableSingletonClass.{u1} α _inst_1], Exists.{succ u1} (α -> Nat -> Bool) (fun (f : α -> Nat -> Bool) => And (Measurable.{u1, 0} α (Nat -> Bool) _inst_1 (MeasurableSpace.pi.{0, 0} Nat (fun (ᾰ : Nat) => Bool) (fun (a : Nat) => instMeasurableSpaceBool)) f) (Function.Injective.{succ u1, 1} α (Nat -> Bool) f))
+Case conversion may be inaccurate. Consider using '#align measurable_space.measurable_injection_cantor_of_countably_generated MeasurableSpace.measurable_injection_cantor_of_countablyGeneratedₓ'. -/
 /-- If a measurable space is countably generated, it admits a measurable injection
 into the Cantor space `ℕ → bool` (equipped with the product sigma algebra). -/
 theorem measurable_injection_cantor_of_countablyGenerated [MeasurableSpace α]

Mathbin/Topology/Perfect.lean

@@ -404,6 +404,12 @@ theorem Perfect.exists_nat_bool_injection [CompleteSpace α] :
 
 end CantorInjMetric
 
+/- warning: is_closed.exists_nat_bool_injection_of_not_countable -> IsClosed.exists_nat_bool_injection_of_not_countable is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} α] [_inst_2 : PolishSpace.{u1} α _inst_1] {C : Set.{u1} α}, (IsClosed.{u1} α _inst_1 C) -> (Not (Set.Countable.{u1} α C)) -> (Exists.{succ u1} ((Nat -> Bool) -> α) (fun (f : (Nat -> Bool) -> α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.hasSubset.{u1} α) (Set.range.{u1, 1} α (Nat -> Bool) f) C) (And (Continuous.{0, u1} (Nat -> Bool) α (Pi.topologicalSpace.{0, 0} Nat (fun (ᾰ : Nat) => Bool) (fun (a : Nat) => Bool.topologicalSpace)) _inst_1 f) (Function.Injective.{1, succ u1} (Nat -> Bool) α f))))
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} α] [_inst_2 : PolishSpace.{u1} α _inst_1] {C : Set.{u1} α}, (IsClosed.{u1} α _inst_1 C) -> (Not (Set.Countable.{u1} α C)) -> (Exists.{succ u1} ((Nat -> Bool) -> α) (fun (f : (Nat -> Bool) -> α) => And (HasSubset.Subset.{u1} (Set.{u1} α) (Set.instHasSubsetSet.{u1} α) (Set.range.{u1, 1} α (Nat -> Bool) f) C) (And (Continuous.{0, u1} (Nat -> Bool) α (Pi.topologicalSpace.{0, 0} Nat (fun (ᾰ : Nat) => Bool) (fun (a : Nat) => instTopologicalSpaceBool)) _inst_1 f) (Function.Injective.{1, succ u1} (Nat -> Bool) α f))))
+Case conversion may be inaccurate. Consider using '#align is_closed.exists_nat_bool_injection_of_not_countable IsClosed.exists_nat_bool_injection_of_not_countableₓ'. -/
 /-- Any closed uncountable subset of a Polish space admits a continuous injection
 from the Cantor space `ℕ → bool`.-/
 theorem IsClosed.exists_nat_bool_injection_of_not_countable {α : Type _} [TopologicalSpace α]

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2d221f4057768209837f353f6222864054677b8b",
+    "rev": "37f514c767cd8c6dcf54df2d22325f7d06520003",
     "name": "lean3port",
-    "inputRev?": "2d221f4057768209837f353f6222864054677b8b"}},
+    "inputRev?": "37f514c767cd8c6dcf54df2d22325f7d06520003"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "1a35e03b62cc967b25c7be2f624fbbd278a0bc09",
+    "rev": "36c927042863b90891eea13554ea68fb66865df6",
     "name": "mathlib",
-    "inputRev?": "1a35e03b62cc967b25c7be2f624fbbd278a0bc09"}},
+    "inputRev?": "36c927042863b90891eea13554ea68fb66865df6"}},
   {"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-04-27-22"
+def tag : String := "nightly-2023-04-28-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"@"2d221f4057768209837f353f6222864054677b8b"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"37f514c767cd8c6dcf54df2d22325f7d06520003"
 
 @[default_target]
 lean_lib Mathbin where