bump to nightly-2023-06-11-17

mathlib commit leanprover-community/mathlib@c471da7

Mathbin/Algebra/Category/Group/Basic.lean

@@ -121,13 +121,11 @@ theorem ext (G H : GroupCat) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x)
 #align Group.ext GroupCat.ext
 #align AddGroup.ext AddGroupCat.ext
 
-#print GroupCat.hasForgetToMonCat /-
 @[to_additive has_forget_to_AddMon]
 instance hasForgetToMonCat : HasForget₂ GroupCat MonCat :=
   BundledHom.forget₂ _ _
 #align Group.has_forget_to_Mon GroupCat.hasForgetToMonCat
 #align AddGroup.has_forget_to_AddMon AddGroupCat.hasForgetToAddMonCat
--/
 
 @[to_additive]
 instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
@@ -238,24 +236,20 @@ theorem ext (G H : CommGroupCat) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂
 #align CommGroup.ext CommGroupCat.ext
 #align AddCommGroup.ext AddCommGroupCat.ext
 
-#print CommGroupCat.hasForgetToGroup /-
 @[to_additive has_forget_to_AddGroup]
 instance hasForgetToGroup : HasForget₂ CommGroupCat GroupCat :=
   BundledHom.forget₂ _ _
 #align CommGroup.has_forget_to_Group CommGroupCat.hasForgetToGroup
 #align AddCommGroup.has_forget_to_AddGroup AddCommGroupCat.hasForgetToAddGroup
--/
 
 @[to_additive]
 instance : Coe CommGroupCat.{u} GroupCat.{u} where coe := (forget₂ CommGroupCat GroupCat).obj
 
-#print CommGroupCat.hasForgetToCommMonCat /-
 @[to_additive has_forget_to_AddCommMon]
 instance hasForgetToCommMonCat : HasForget₂ CommGroupCat CommMonCat :=
   InducedCategory.hasForget₂ fun G : CommGroupCat => CommMonCat.of G
 #align CommGroup.has_forget_to_CommMon CommGroupCat.hasForgetToCommMonCat
 #align AddCommGroup.has_forget_to_AddCommMon AddCommGroupCat.hasForgetToAddCommMonCat
--/
 
 @[to_additive]
 instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj

Mathbin/Algebra/Category/Module/Basic.lean

@@ -110,13 +110,11 @@ instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R)
 #align Module.Module_concrete_category ModuleCat.moduleConcreteCategory
 -/
 
-#print ModuleCat.hasForgetToAddCommGroup /-
 instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGroupCat
     where forget₂ :=
     { obj := fun M => AddCommGroupCat.of M
       map := fun M₁ M₂ f => LinearMap.toAddMonoidHom f }
 #align Module.has_forget_to_AddCommGroup ModuleCat.hasForgetToAddCommGroup
--/
 
 instance (M N : ModuleCat R) : LinearMapClass (M ⟶ N) R M N :=
   { LinearMap.semilinearMapClass with coe := fun f => f }

Mathbin/Algebra/Category/Module/FilteredColimits.lean

@@ -54,19 +54,19 @@ parameter (F : J ⥤ ModuleCat.{max v u} R)
 /-- The colimit of `F ⋙ forget₂ (Module R) AddCommGroup` in the category `AddCommGroup`.
 In the following, we will show that this has the structure of an `R`-module.
 -/
-abbrev m : AddCommGroupCat :=
+abbrev M : AddCommGroupCat :=
   AddCommGroupCat.FilteredColimits.colimit (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat.{max v u})
-#align Module.filtered_colimits.M ModuleCat.FilteredColimits.m
+#align Module.filtered_colimits.M ModuleCat.FilteredColimits.M
 
 /-- The canonical projection into the colimit, as a quotient type. -/
-abbrev m.mk : (Σ j, F.obj j) → M :=
+abbrev M.mk : (Σ j, F.obj j) → M :=
   Quot.mk (Types.Quot.Rel (F ⋙ forget (ModuleCat R)))
-#align Module.filtered_colimits.M.mk ModuleCat.FilteredColimits.m.mk
+#align Module.filtered_colimits.M.mk ModuleCat.FilteredColimits.M.mk
 
-theorem m.mk_eq (x y : Σ j, F.obj j)
+theorem M.mk_eq (x y : Σ j, F.obj j)
     (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) : M.mk x = M.mk y :=
   Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget (ModuleCat R)) x y h)
-#align Module.filtered_colimits.M.mk_eq ModuleCat.FilteredColimits.m.mk_eq
+#align Module.filtered_colimits.M.mk_eq ModuleCat.FilteredColimits.M.mk_eq
 
 /-- The "unlifted" version of scalar multiplication in the colimit. -/
 def colimitSmulAux (r : R) (x : Σ j, F.obj j) : M :=
@@ -184,6 +184,7 @@ def colimitCoconeIsColimit : IsColimit colimit_cocone
         ((forget (ModuleCat R)).mapCocone t) m fun j => funext fun x => LinearMap.congr_fun (h j) x
 #align Module.filtered_colimits.colimit_cocone_is_colimit ModuleCat.FilteredColimits.colimitCoconeIsColimit
 
+#print ModuleCat.FilteredColimits.forget₂AddCommGroupPreservesFilteredColimits /-
 instance forget₂AddCommGroupPreservesFilteredColimits :
     PreservesFilteredColimits (forget₂ (ModuleCat R) AddCommGroupCat.{u})
     where PreservesFilteredColimits J _ _ :=
@@ -193,11 +194,14 @@ instance forget₂AddCommGroupPreservesFilteredColimits :
           (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit
             (F ⋙ forget₂ (ModuleCat.{u} R) AddCommGroupCat.{u})) }
 #align Module.filtered_colimits.forget₂_AddCommGroup_preserves_filtered_colimits ModuleCat.FilteredColimits.forget₂AddCommGroupPreservesFilteredColimits
+-/
 
+#print ModuleCat.FilteredColimits.forgetPreservesFilteredColimits /-
 instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget (ModuleCat.{u} R)) :=
   Limits.compPreservesFilteredColimits (forget₂ (ModuleCat R) AddCommGroupCat)
     (forget AddCommGroupCat)
 #align Module.filtered_colimits.forget_preserves_filtered_colimits ModuleCat.FilteredColimits.forgetPreservesFilteredColimits
+-/
 
 end
 

Mathbin/Algebra/Category/Mon/Basic.lean

@@ -186,13 +186,11 @@ theorem coe_of (R : Type u) [CommMonoid R] : (CommMonCat.of R : Type u) = R :=
 #align AddCommMon.coe_of AddCommMonCat.coe_of
 -/
 
-#print CommMonCat.hasForgetToMonCat /-
 @[to_additive has_forget_to_AddMon]
 instance hasForgetToMonCat : HasForget₂ CommMonCat MonCat :=
   BundledHom.forget₂ _ _
 #align CommMon.has_forget_to_Mon CommMonCat.hasForgetToMonCat
 #align AddCommMon.has_forget_to_AddMon AddCommMonCat.hasForgetToAddMonCat
--/
 
 @[to_additive]
 instance : Coe CommMonCat.{u} MonCat.{u} where coe := (forget₂ CommMonCat MonCat).obj

Mathbin/Algebra/Category/Ring/Basic.lean

@@ -95,21 +95,17 @@ theorem coe_of (R : Type u) [Semiring R] : (SemiRingCat.of R : Type u) = R :=
 #align SemiRing.coe_of SemiRingCat.coe_of
 -/
 
-#print SemiRingCat.hasForgetToMonCat /-
 instance hasForgetToMonCat : HasForget₂ SemiRingCat MonCat :=
   BundledHom.mkHasForget₂ (fun R hR => @MonoidWithZero.toMonoid R (@Semiring.toMonoidWithZero R hR))
     (fun R₁ R₂ => RingHom.toMonoidHom) fun _ _ _ => rfl
 #align SemiRing.has_forget_to_Mon SemiRingCat.hasForgetToMonCat
--/
 
-#print SemiRingCat.hasForgetToAddCommMonCat /-
 instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat
     where-- can't use bundled_hom.mk_has_forget₂, since AddCommMon is an induced category
   forget₂ :=
     { obj := fun R => AddCommMonCat.of R
       map := fun R₁ R₂ f => RingHom.toAddMonoidHom f }
 #align SemiRing.has_forget_to_AddCommMon SemiRingCat.hasForgetToAddCommMonCat
--/
 
 end SemiRingCat
 
@@ -163,20 +159,16 @@ theorem coe_of (R : Type u) [Ring R] : (RingCat.of R : Type u) = R :=
 #align Ring.coe_of RingCat.coe_of
 -/
 
-#print RingCat.hasForgetToSemiRingCat /-
 instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat :=
   BundledHom.forget₂ _ _
 #align Ring.has_forget_to_SemiRing RingCat.hasForgetToSemiRingCat
--/
 
-#print RingCat.hasForgetToAddCommGroupCat /-
 instance hasForgetToAddCommGroupCat : HasForget₂ RingCat AddCommGroupCat
     where-- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category
   forget₂ :=
     { obj := fun R => AddCommGroupCat.of R
       map := fun R₁ R₂ f => RingHom.toAddMonoidHom f }
 #align Ring.has_forget_to_AddCommGroup RingCat.hasForgetToAddCommGroupCat
--/
 
 end RingCat
 
@@ -230,19 +222,15 @@ theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRing.of R : Type u) = R
 #align CommSemiRing.coe_of CommSemiRing.coe_of
 -/
 
-#print CommSemiRing.hasForgetToSemiRingCat /-
 instance hasForgetToSemiRingCat : HasForget₂ CommSemiRingCat SemiRingCat :=
   BundledHom.forget₂ _ _
 #align CommSemiRing.has_forget_to_SemiRing CommSemiRing.hasForgetToSemiRingCat
--/
 
-#print CommSemiRing.hasForgetToCommMonCat /-
 /-- 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
--/
 
 end CommSemiRingCat
 
@@ -296,19 +284,15 @@ theorem coe_of (R : Type u) [CommRing R] : (CommRingCat.of R : Type u) = R :=
 #align CommRing.coe_of CommRingCat.coe_of
 -/
 
-#print CommRingCat.hasForgetToRingCat /-
 instance hasForgetToRingCat : HasForget₂ CommRingCat RingCat :=
   BundledHom.forget₂ _ _
 #align CommRing.has_forget_to_Ring CommRingCat.hasForgetToRingCat
--/
 
-#print CommRingCat.hasForgetToCommSemiRingCat /-
 /-- 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)
     (by tidy)
 #align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRingCat
--/
 
 instance : Full (forget₂ CommRingCat CommSemiRingCat) where preimage X Y f := f
 

Mathbin/Analysis/NormedSpace/Algebra.lean

@@ -43,7 +43,7 @@ variable [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [C
 theorem norm_le_norm_one (φ : characterSpace 𝕜 A) : ‖toNormedDual (φ : WeakDual 𝕜 A)‖ ≤ ‖(1 : A)‖ :=
   ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg (1 : A)) fun a =>
     mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ a)
-#align weak_dual.character_space.norm_le_norm_one WeakDual.characterSpace.norm_le_norm_one
+#align weak_dual.character_space.norm_le_norm_one WeakDual.CharacterSpace.norm_le_norm_one
 
 instance [ProperSpace 𝕜] : CompactSpace (characterSpace 𝕜 A) :=
   by

Mathbin/Analysis/NormedSpace/Spectrum.lean

@@ -50,6 +50,7 @@ This file contains the basic theory for the resolvent and spectrum of a Banach a
 
 open scoped ENNReal NNReal
 
+#print spectralRadius /-
 /-- The *spectral radius* is the supremum of the `nnnorm` (`‖⬝‖₊`) of elements in the spectrum,
     coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
     case, `spectral_radius a = 0`.  It is also possible that `spectrum 𝕜 a` be unbounded (though
@@ -59,6 +60,7 @@ noncomputable def spectralRadius (𝕜 : Type _) {A : Type _} [NormedField 𝕜]
     (a : A) : ℝ≥0∞ :=
   ⨆ k ∈ spectrum 𝕜 a, ‖k‖₊
 #align spectral_radius spectralRadius
+-/
 
 variable {𝕜 : Type _} {A : Type _}
 
@@ -574,11 +576,13 @@ instance (priority := 100) [AlgHomClass F 𝕜 A 𝕜] : ContinuousLinearMapClas
       AddMonoidHomClass.continuous_of_bound φ ‖(1 : A)‖ fun a =>
         mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ _) }
 
+#print AlgHom.toContinuousLinearMap /-
 /-- An algebra homomorphism into the base field, as a continuous linear map (since it is
 automatically bounded). -/
 def toContinuousLinearMap (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
   { φ.toLinearMap with cont := map_continuous φ }
 #align alg_hom.to_continuous_linear_map AlgHom.toContinuousLinearMap
+-/
 
 @[simp]
 theorem coe_toContinuousLinearMap (φ : A →ₐ[𝕜] 𝕜) : ⇑φ.toContinuousLinearMap = φ :=
@@ -623,6 +627,7 @@ variable [NontriviallyNormedField 𝕜] [NormedRing A] [CompleteSpace A]
 
 variable [NormedAlgebra 𝕜 A]
 
+#print WeakDual.CharacterSpace.equivAlgHom /-
 /-- The equivalence between characters and algebra homomorphisms into the base field. -/
 def equivAlgHom : characterSpace 𝕜 A ≃ (A →ₐ[𝕜] 𝕜)
     where
@@ -632,17 +637,18 @@ def equivAlgHom : characterSpace 𝕜 A ≃ (A →ₐ[𝕜] 𝕜)
       property := by rw [eq_set_map_one_map_mul]; exact ⟨map_one f, map_mul f⟩ }
   left_inv f := Subtype.ext <| ContinuousLinearMap.ext fun x => rfl
   right_inv f := AlgHom.ext fun x => rfl
-#align weak_dual.character_space.equiv_alg_hom WeakDual.characterSpace.equivAlgHom
+#align weak_dual.character_space.equiv_alg_hom WeakDual.CharacterSpace.equivAlgHom
+-/
 
 @[simp]
 theorem equivAlgHom_coe (f : characterSpace 𝕜 A) : ⇑(equivAlgHom f) = f :=
   rfl
-#align weak_dual.character_space.equiv_alg_hom_coe WeakDual.characterSpace.equivAlgHom_coe
+#align weak_dual.character_space.equiv_alg_hom_coe WeakDual.CharacterSpace.equivAlgHom_coe
 
 @[simp]
 theorem equivAlgHom_symm_coe (f : A →ₐ[𝕜] 𝕜) : ⇑(equivAlgHom.symm f) = f :=
   rfl
-#align weak_dual.character_space.equiv_alg_hom_symm_coe WeakDual.characterSpace.equivAlgHom_symm_coe
+#align weak_dual.character_space.equiv_alg_hom_symm_coe WeakDual.CharacterSpace.equivAlgHom_symm_coe
 
 end CharacterSpace
 

Mathbin/Analysis/NormedSpace/Star/GelfandDuality.lean

@@ -76,7 +76,7 @@ algebra. In particular, the character, which may be identified as an algebra hom
 `weak_dual.character_space.equiv_alg_hom`, is given by the composition of the quotient map and
 the Gelfand-Mazur isomorphism `normed_ring.alg_equiv_complex_of_complete`. -/
 noncomputable def Ideal.toCharacterSpace : characterSpace ℂ A :=
-  characterSpace.equivAlgHom.symm <|
+  CharacterSpace.equivAlgHom.symm <|
     ((@NormedRing.algEquivComplexOfComplete (A ⧸ I) _ _
               (letI := quotient.field I
               @isUnit_iff_ne_zero (A ⧸ I) _)

Mathbin/CategoryTheory/Category/Twop.lean

@@ -94,11 +94,9 @@ instance concreteCategory : ConcreteCategory TwoP :=
 #align Twop.concrete_category TwoP.concreteCategory
 -/
 
-#print TwoP.hasForgetToBipointed /-
 instance hasForgetToBipointed : HasForget₂ TwoP Bipointed :=
   InducedCategory.hasForget₂ toBipointed
 #align Twop.has_forget_to_Bipointed TwoP.hasForgetToBipointed
--/
 
 #print TwoP.swap /-
 /-- Swaps the pointed elements of a two-pointed type. `two_pointing.swap` as a functor. -/

Mathbin/CategoryTheory/ConcreteCategory/Basic.lean

@@ -206,7 +206,6 @@ theorem ConcreteCategory.hasCoeToFun_Type {X Y : Type u} (f : X ⟶ Y) : coeFn f
 
 end
 
-#print CategoryTheory.HasForget₂ /-
 /-- `has_forget₂ C D`, where `C` and `D` are both concrete categories, provides a functor
 `forget₂ C D : C ⥤ D` and a proof that `forget₂ ⋙ (forget D) = forget C`.
 -/
@@ -215,60 +214,47 @@ class HasForget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory.{u}
   forget₂ : C ⥤ D
   forget_comp : forget₂ ⋙ forget D = forget C := by obviously
 #align category_theory.has_forget₂ CategoryTheory.HasForget₂
--/
 
-#print CategoryTheory.forget₂ /-
 /-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance
 `has_forget₂ C `. -/
 @[reducible]
 def forget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory C] [Category D]
     [ConcreteCategory D] [HasForget₂ C D] : C ⥤ D :=
   HasForget₂.forget₂
 #align category_theory.forget₂ CategoryTheory.forget₂
--/
 
-#print CategoryTheory.forget₂_faithful /-
 instance forget₂_faithful (C : Type v) (D : Type v') [Category C] [ConcreteCategory C] [Category D]
     [ConcreteCategory D] [HasForget₂ C D] : Faithful (forget₂ C D) :=
   HasForget₂.forget_comp.faithful_of_comp
 #align category_theory.forget₂_faithful CategoryTheory.forget₂_faithful
--/
 
-#print CategoryTheory.forget₂_preservesMonomorphisms /-
 instance forget₂_preservesMonomorphisms (C : Type v) (D : Type v') [Category C] [ConcreteCategory C]
     [Category D] [ConcreteCategory D] [HasForget₂ C D] [(forget C).PreservesMonomorphisms] :
     (forget₂ C D).PreservesMonomorphisms :=
   have : (forget₂ C D ⋙ forget D).PreservesMonomorphisms := by simp only [has_forget₂.forget_comp];
     infer_instance
   functor.preserves_monomorphisms_of_preserves_of_reflects _ (forget D)
 #align category_theory.forget₂_preserves_monomorphisms CategoryTheory.forget₂_preservesMonomorphisms
--/
 
-#print CategoryTheory.forget₂_preservesEpimorphisms /-
 instance forget₂_preservesEpimorphisms (C : Type v) (D : Type v') [Category C] [ConcreteCategory C]
     [Category D] [ConcreteCategory D] [HasForget₂ C D] [(forget C).PreservesEpimorphisms] :
     (forget₂ C D).PreservesEpimorphisms :=
   have : (forget₂ C D ⋙ forget D).PreservesEpimorphisms := by simp only [has_forget₂.forget_comp];
     infer_instance
   functor.preserves_epimorphisms_of_preserves_of_reflects _ (forget D)
 #align category_theory.forget₂_preserves_epimorphisms CategoryTheory.forget₂_preservesEpimorphisms
--/
 
-#print CategoryTheory.InducedCategory.concreteCategory /-
 instance InducedCategory.concreteCategory {C : Type v} {D : Type v'} [Category D]
     [ConcreteCategory D] (f : C → D) : ConcreteCategory (InducedCategory D f)
     where forget := inducedFunctor f ⋙ forget D
 #align category_theory.induced_category.concrete_category CategoryTheory.InducedCategory.concreteCategory
--/
 
-#print CategoryTheory.InducedCategory.hasForget₂ /-
 instance InducedCategory.hasForget₂ {C : Type v} {D : Type v'} [Category D] [ConcreteCategory D]
     (f : C → D) : HasForget₂ (InducedCategory D f) D
     where
   forget₂ := inducedFunctor f
   forget_comp := rfl
 #align category_theory.induced_category.has_forget₂ CategoryTheory.InducedCategory.hasForget₂
--/
 
 instance FullSubcategory.concreteCategory {C : Type v} [Category C] [ConcreteCategory C]
     (Z : C → Prop) : ConcreteCategory (FullSubcategory Z)
@@ -294,15 +280,13 @@ def HasForget₂.mk' {C : Type v} {D : Type v'} [Category C] [ConcreteCategory C
   forget_comp := by apply faithful.div_comp
 #align category_theory.has_forget₂.mk' CategoryTheory.HasForget₂.mk'
 
-#print CategoryTheory.hasForgetToType /-
 /-- Every forgetful functor factors through the identity functor. This is not a global instance as
     it is prone to creating type class resolution loops. -/
 def hasForgetToType (C : Type v) [Category C] [ConcreteCategory C] : HasForget₂ C (Type u)
     where
   forget₂ := forget C
   forget_comp := Functor.comp_id _
 #align category_theory.has_forget_to_Type CategoryTheory.hasForgetToType
--/
 
 end CategoryTheory