bump to nightly-2023-06-13-03

mathlib commit leanprover-community/mathlib@9fb8964

Mathbin/Algebra/Category/Module/FilteredColimits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Justus Springer
 
 ! This file was ported from Lean 3 source module algebra.category.Module.filtered_colimits
-! leanprover-community/mathlib commit 806bbb0132ba63b93d5edbe4789ea226f8329979
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Category.Module.Basic
 /-!
 # The forgetful functor from `R`-modules preserves filtered colimits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
 to preserve _filtered_ colimits.
 

Mathbin/Algebra/Category/Ring/Basic.lean

@@ -189,18 +189,18 @@ deriving instance LargeCategory, ConcreteCategory for CommSemiRingCat
 instance : CoeSort CommSemiRingCat (Type _) :=
   Bundled.hasCoeToSort
 
-#print CommSemiRing.of /-
+#print CommSemiRingCat.of /-
 /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [CommSemiring R] : CommSemiRingCat :=
   Bundled.of R
-#align CommSemiRing.of CommSemiRing.of
+#align CommSemiRing.of CommSemiRingCat.of
 -/
 
-#print CommSemiRing.ofHom /-
+#print CommSemiRingCat.ofHom /-
 /-- Typecheck a `ring_hom` as a morphism in `CommSemiRing`. -/
 def ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : of R ⟶ of S :=
   f
-#align CommSemiRing.of_hom CommSemiRing.ofHom
+#align CommSemiRing.of_hom CommSemiRingCat.ofHom
 -/
 
 @[simp]
@@ -215,22 +215,22 @@ instance : Inhabited CommSemiRingCat :=
 instance (R : CommSemiRingCat) : CommSemiring R :=
   R.str
 
-#print CommSemiRing.coe_of /-
+#print CommSemiRingCat.coe_of /-
 @[simp]
-theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRing.of R : Type u) = R :=
+theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRingCat.of R : Type u) = R :=
   rfl
-#align CommSemiRing.coe_of CommSemiRing.coe_of
+#align CommSemiRing.coe_of CommSemiRingCat.coe_of
 -/
 
 instance hasForgetToSemiRingCat : HasForget₂ CommSemiRingCat SemiRingCat :=
   BundledHom.forget₂ _ _
-#align CommSemiRing.has_forget_to_SemiRing CommSemiRing.hasForgetToSemiRingCat
+#align CommSemiRing.has_forget_to_SemiRing CommSemiRingCat.hasForgetToSemiRingCat
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat :=
   HasForget₂.mk' (fun R : CommSemiRingCat => CommMonCat.of R) (fun R => rfl)
     (fun R₁ R₂ f => f.toMonoidHom) (by tidy)
-#align CommSemiRing.has_forget_to_CommMon CommSemiRing.hasForgetToCommMonCat
+#align CommSemiRing.has_forget_to_CommMon CommSemiRingCat.hasForgetToCommMonCat
 
 end CommSemiRingCat
 
@@ -290,7 +290,7 @@ instance hasForgetToRingCat : HasForget₂ CommRingCat RingCat :=
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance hasForgetToCommSemiRingCat : HasForget₂ CommRingCat CommSemiRingCat :=
-  HasForget₂.mk' (fun R : CommRingCat => CommSemiRing.of R) (fun R => rfl) (fun R₁ R₂ f => f)
+  HasForget₂.mk' (fun R : CommRingCat => CommSemiRingCat.of R) (fun R => rfl) (fun R₁ R₂ f => f)
     (by tidy)
 #align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRingCat
 

Mathbin/Algebra/Category/Ring/FilteredColimits.lean

@@ -217,7 +217,7 @@ instance colimitCommSemiring : CommSemiring R :=
 #print CommSemiRingCat.FilteredColimits.colimit /-
 /-- The bundled commutative semiring giving the filtered colimit of a diagram. -/
 def colimit : CommSemiRingCat :=
-  CommSemiRing.of R
+  CommSemiRingCat.of R
 #align CommSemiRing.filtered_colimits.colimit CommSemiRingCat.FilteredColimits.colimit
 -/
 

Mathbin/Algebra/Category/Ring/Limits.lean

@@ -231,7 +231,7 @@ instance (F : J ⥤ CommSemiRingCat.{max v u}) :
     CreatesLimit F (forget₂ CommSemiRingCat SemiRingCat.{max v u}) :=
   createsLimitOfReflectsIso fun c' t =>
     { liftedCone :=
-        { pt := CommSemiRing.of (Types.limitCone (F ⋙ forget _)).pt
+        { pt := CommSemiRingCat.of (Types.limitCone (F ⋙ forget _)).pt
           π :=
             { app := by
                 apply SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})

Mathbin/All.lean

@@ -2168,9 +2168,13 @@ import Mathbin.MeasureTheory.Function.AeEqFun
 import Mathbin.MeasureTheory.Function.AeEqOfIntegral
 import Mathbin.MeasureTheory.Function.AeMeasurableOrder
 import Mathbin.MeasureTheory.Function.AeMeasurableSequence
+import Mathbin.MeasureTheory.Function.ConditionalExpectation.AeMeasurable
 import Mathbin.MeasureTheory.Function.ConditionalExpectation.Basic
+import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL1
+import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL2
 import Mathbin.MeasureTheory.Function.ConditionalExpectation.Indicator
 import Mathbin.MeasureTheory.Function.ConditionalExpectation.Real
+import Mathbin.MeasureTheory.Function.ConditionalExpectation.Unique
 import Mathbin.MeasureTheory.Function.ContinuousMapDense
 import Mathbin.MeasureTheory.Function.ConvergenceInMeasure
 import Mathbin.MeasureTheory.Function.Egorov

Mathbin/Analysis/NormedSpace/Algebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 
 ! This file was ported from Lean 3 source module analysis.normed_space.algebra
-! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.NormedSpace.Spectrum
 /-!
 # Normed algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains basic facts about normed algebras.
 
 ## Main results

Mathbin/Analysis/NormedSpace/Spectrum.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.spectrum
-! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.Analysis.NormedSpace.Exponential
 /-!
 # The spectrum of elements in a complete normed algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains the basic theory for the resolvent and spectrum of a Banach algebra.
 
 ## Main definitions

Mathbin/Analysis/NormedSpace/Star/GelfandDuality.lean

@@ -4,7 +4,7 @@ Reeased under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.gelfand_duality
-! leanprover-community/mathlib commit e65771194f9e923a70dfb49b6ca7be6e400d8b6f
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -19,6 +19,9 @@ import Mathbin.Topology.ContinuousFunction.StoneWeierstrass
 /-!
 # Gelfand Duality
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The `gelfand_transform` is an algebra homomorphism from a topological `𝕜`-algebra `A` to
 `C(character_space 𝕜 A, 𝕜)`. In the case where `A` is a commutative complex Banach algebra, then
 the Gelfand transform is actually spectrum-preserving (`spectrum.gelfand_transform_eq`). Moreover,

Mathbin/Analysis/NormedSpace/Star/Spectrum.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.spectrum
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.SpecialFunctions.Exponential
 import Mathbin.Algebra.Star.StarAlgHom
 
 /-! # Spectral properties in C⋆-algebras
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In this file, we establish various properties related to the spectrum of elements in C⋆-algebras.
 -/
 

Mathbin/CategoryTheory/ConcreteCategory/Basic.lean

@@ -197,12 +197,10 @@ theorem ConcreteCategory.bijective_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] :
     Function.Bijective ((forget C).map f) := by rw [← is_iso_iff_bijective]; infer_instance
 #align category_theory.concrete_category.bijective_of_is_iso CategoryTheory.ConcreteCategory.bijective_of_isIso
 
-#print CategoryTheory.ConcreteCategory.hasCoeToFun_Type /-
 @[simp]
 theorem ConcreteCategory.hasCoeToFun_Type {X Y : Type u} (f : X ⟶ Y) : coeFn f = f :=
   rfl
 #align category_theory.concrete_category.has_coe_to_fun_Type CategoryTheory.ConcreteCategory.hasCoeToFun_Type
--/
 
 end
 

Mathbin/CategoryTheory/Limits/ConcreteCategory.lean

@@ -70,7 +70,6 @@ open WidePullback
 
 open WidePullbackShape
 
-#print CategoryTheory.Limits.Concrete.widePullback_ext /-
 theorem Concrete.widePullback_ext {B : C} {ι : Type w} {X : ι → C} (f : ∀ j : ι, X j ⟶ B)
     [HasWidePullback B X f] [PreservesLimit (wideCospan B X f) (forget C)]
     (x y : widePullback B X f) (h₀ : base f x = base f y) (h : ∀ j, π f j x = π f j y) : x = y :=
@@ -80,9 +79,7 @@ theorem Concrete.widePullback_ext {B : C} {ι : Type w} {X : ι → C} (f : ∀
   · exact h₀
   · apply h
 #align category_theory.limits.concrete.wide_pullback_ext CategoryTheory.Limits.Concrete.widePullback_ext
--/
 
-#print CategoryTheory.Limits.Concrete.widePullback_ext' /-
 theorem Concrete.widePullback_ext' {B : C} {ι : Type w} [Nonempty ι] {X : ι → C}
     (f : ∀ j : ι, X j ⟶ B) [HasWidePullback.{w} B X f]
     [PreservesLimit (wideCospan B X f) (forget C)] (x y : widePullback B X f)
@@ -92,13 +89,11 @@ theorem Concrete.widePullback_ext' {B : C} {ι : Type w} [Nonempty ι] {X : ι 
   inhabit ι
   simp only [← π_arrow f (Inhabited.default _), comp_apply, h]
 #align category_theory.limits.concrete.wide_pullback_ext' CategoryTheory.Limits.Concrete.widePullback_ext'
--/
 
 end WidePullback
 
 section Multiequalizer
 
-#print CategoryTheory.Limits.Concrete.multiequalizer_ext /-
 theorem Concrete.multiequalizer_ext {I : MulticospanIndex.{w} C} [HasMultiequalizer I]
     [PreservesLimit I.multicospan (forget C)] (x y : multiequalizer I)
     (h : ∀ t : I.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y :=
@@ -108,7 +103,6 @@ theorem Concrete.multiequalizer_ext {I : MulticospanIndex.{w} C} [HasMultiequali
   · apply h
   · rw [← limit.w I.multicospan (walking_multicospan.hom.fst b), comp_apply, comp_apply, h]
 #align category_theory.limits.concrete.multiequalizer_ext CategoryTheory.Limits.Concrete.multiequalizer_ext
--/
 
 /-- An auxiliary equivalence to be used in `multiequalizer_equiv` below.-/
 def Concrete.multiequalizerEquivAux (I : MulticospanIndex C) :
@@ -142,7 +136,6 @@ def Concrete.multiequalizerEquivAux (I : MulticospanIndex C) :
   right_inv := by intro x; ext i; rfl
 #align category_theory.limits.concrete.multiequalizer_equiv_aux CategoryTheory.Limits.Concrete.multiequalizerEquivAux
 
-#print CategoryTheory.Limits.Concrete.multiequalizerEquiv /-
 /-- The equivalence between the noncomputable multiequalizer and
 and the concrete multiequalizer. -/
 noncomputable def Concrete.multiequalizerEquiv (I : MulticospanIndex.{w} C) [HasMultiequalizer I]
@@ -154,7 +147,6 @@ noncomputable def Concrete.multiequalizerEquiv (I : MulticospanIndex.{w} C) [Has
   let E := h2.conePointUniqueUpToIso (Types.limitConeIsLimit _)
   Equiv.trans E.toEquiv (Concrete.multiequalizerEquivAux I)
 #align category_theory.limits.concrete.multiequalizer_equiv CategoryTheory.Limits.Concrete.multiequalizerEquiv
--/
 
 @[simp]
 theorem Concrete.multiequalizerEquiv_apply (I : MulticospanIndex.{w} C) [HasMultiequalizer I]
@@ -322,7 +314,6 @@ open WidePushout
 
 open WidePushoutShape
 
-#print CategoryTheory.Limits.Concrete.widePushout_exists_rep /-
 theorem Concrete.widePushout_exists_rep {B : C} {α : Type _} {X : α → C} (f : ∀ j : α, B ⟶ X j)
     [HasWidePushout.{v} B X f] [PreservesColimit (wideSpan B X f) (forget C)]
     (x : widePushout B X f) : (∃ y : B, head f y = x) ∨ ∃ (i : α) (y : X i), ι f i y = x :=
@@ -332,9 +323,7 @@ theorem Concrete.widePushout_exists_rep {B : C} {α : Type _} {X : α → C} (f
   · right
     use j, y
 #align category_theory.limits.concrete.wide_pushout_exists_rep CategoryTheory.Limits.Concrete.widePushout_exists_rep
--/
 
-#print CategoryTheory.Limits.Concrete.widePushout_exists_rep' /-
 theorem Concrete.widePushout_exists_rep' {B : C} {α : Type _} [Nonempty α] {X : α → C}
     (f : ∀ j : α, B ⟶ X j) [HasWidePushout.{v} B X f] [PreservesColimit (wideSpan B X f) (forget C)]
     (x : widePushout B X f) : ∃ (i : α) (y : X i), ι f i y = x :=
@@ -345,7 +334,6 @@ theorem Concrete.widePushout_exists_rep' {B : C} {α : Type _} [Nonempty α] {X
     simp only [← arrow_ι _ (Inhabited.default α), comp_apply]
   · use i, y
 #align category_theory.limits.concrete.wide_pushout_exists_rep' CategoryTheory.Limits.Concrete.widePushout_exists_rep'
--/
 
 end WidePushout
 

Mathbin/CategoryTheory/Sites/Sheafification.lean

@@ -138,7 +138,6 @@ theorem equiv_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.cover X} [HasMultiequaliz
   rfl
 #align category_theory.meq.equiv_apply CategoryTheory.Meq.equiv_apply
 
-#print CategoryTheory.Meq.equiv_symm_eq_apply /-
 @[simp]
 theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.cover X} [HasMultiequalizer (S.index P)]
     (x : Meq P S) (I : S.arrow) : Multiequalizer.ι (S.index P) I ((Meq.equiv P S).symm x) = x I :=
@@ -147,7 +146,6 @@ theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.cover X} [HasMult
   rw [← equiv_apply]
   simp
 #align category_theory.meq.equiv_symm_eq_apply CategoryTheory.Meq.equiv_symm_eq_apply
--/
 
 end Meq
 

Mathbin/CategoryTheory/Sites/Surjective.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module category_theory.sites.surjective
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 087c325ae0ab42dbdd5dee55bc37d3d5a0bf2197
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Sites.CompatibleSheafification
 
 # Locally surjective morphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 - `is_locally_surjective` : A morphism of presheaves valued in a concrete category is locally