bump to nightly-2023-03-08-20

mathlib commit leanprover-community/mathlib@38f16f9

Mathbin/Algebra/Category/Group/Biproducts.lean

@@ -144,7 +144,7 @@ on the dependent function type
 @[simps hom_apply]
 noncomputable def biproductIsoPi (f : J → AddCommGroupCat.{u}) :
     (⨁ f : AddCommGroupCat) ≅ AddCommGroupCat.of (∀ j, f j) :=
-  IsLimit.conePointUniqueUpToIso (Biproduct.isLimit f) (productLimitCone f).IsLimit
+  IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).IsLimit
 #align AddCommGroup.biproduct_iso_pi AddCommGroupCat.biproductIsoPi
 
 @[simp, elementwise]

Mathbin/Algebra/Category/Module/Biproducts.lean

@@ -149,7 +149,7 @@ on the dependent function type
 @[simps hom_apply]
 noncomputable def biproductIsoPi [Fintype J] (f : J → ModuleCat.{v} R) :
     (⨁ f : ModuleCat.{v} R) ≅ ModuleCat.of R (∀ j, f j) :=
-  IsLimit.conePointUniqueUpToIso (Biproduct.isLimit f) (productLimitCone f).IsLimit
+  IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).IsLimit
 #align Module.biproduct_iso_pi ModuleCat.biproductIsoPi
 
 @[simp, elementwise]

Mathbin/CategoryTheory/Abelian/Images.lean

@@ -43,61 +43,82 @@ variable {P Q : C} (f : P ⟶ Q)
 
 section Image
 
+#print CategoryTheory.Abelian.image /-
 /-- The kernel of the cokernel of `f` is called the (abelian) image of `f`. -/
 protected abbrev image : C :=
   kernel (cokernel.π f)
 #align category_theory.abelian.image CategoryTheory.Abelian.image
+-/
 
+#print CategoryTheory.Abelian.image.ι /-
 /-- The inclusion of the image into the codomain. -/
 protected abbrev image.ι : Abelian.image f ⟶ Q :=
   kernel.ι (cokernel.π f)
 #align category_theory.abelian.image.ι CategoryTheory.Abelian.image.ι
+-/
 
+#print CategoryTheory.Abelian.factorThruImage /-
 /-- There is a canonical epimorphism `p : P ⟶ image f` for every `f`. -/
 protected abbrev factorThruImage : P ⟶ Abelian.image f :=
   kernel.lift (cokernel.π f) f <| cokernel.condition f
 #align category_theory.abelian.factor_thru_image CategoryTheory.Abelian.factorThruImage
+-/
 
+#print CategoryTheory.Abelian.image.fac /-
 /-- `f` factors through its image via the canonical morphism `p`. -/
 @[simp, reassoc.1]
 protected theorem image.fac : Abelian.factorThruImage f ≫ image.ι f = f :=
   kernel.lift_ι _ _ _
 #align category_theory.abelian.image.fac CategoryTheory.Abelian.image.fac
+-/
 
+#print CategoryTheory.Abelian.mono_factorThruImage /-
 instance mono_factorThruImage [Mono f] : Mono (Abelian.factorThruImage f) :=
   mono_of_mono_fac <| image.fac f
 #align category_theory.abelian.mono_factor_thru_image CategoryTheory.Abelian.mono_factorThruImage
+-/
 
 end Image
 
 section Coimage
 
+#print CategoryTheory.Abelian.coimage /-
 /-- The cokernel of the kernel of `f` is called the (abelian) coimage of `f`. -/
 protected abbrev coimage : C :=
   cokernel (kernel.ι f)
 #align category_theory.abelian.coimage CategoryTheory.Abelian.coimage
+-/
 
+#print CategoryTheory.Abelian.coimage.π /-
 /-- The projection onto the coimage. -/
 protected abbrev coimage.π : P ⟶ Abelian.coimage f :=
   cokernel.π (kernel.ι f)
 #align category_theory.abelian.coimage.π CategoryTheory.Abelian.coimage.π
+-/
 
+#print CategoryTheory.Abelian.factorThruCoimage /-
 /-- There is a canonical monomorphism `i : coimage f ⟶ Q`. -/
 protected abbrev factorThruCoimage : Abelian.coimage f ⟶ Q :=
   cokernel.desc (kernel.ι f) f <| kernel.condition f
 #align category_theory.abelian.factor_thru_coimage CategoryTheory.Abelian.factorThruCoimage
+-/
 
+#print CategoryTheory.Abelian.coimage.fac /-
 /-- `f` factors through its coimage via the canonical morphism `p`. -/
 protected theorem coimage.fac : coimage.π f ≫ Abelian.factorThruCoimage f = f :=
   cokernel.π_desc _ _ _
 #align category_theory.abelian.coimage.fac CategoryTheory.Abelian.coimage.fac
+-/
 
+#print CategoryTheory.Abelian.epi_factorThruCoimage /-
 instance epi_factorThruCoimage [Epi f] : Epi (Abelian.factorThruCoimage f) :=
   epi_of_epi_fac <| coimage.fac f
 #align category_theory.abelian.epi_factor_thru_coimage CategoryTheory.Abelian.epi_factorThruCoimage
+-/
 
 end Coimage
 
+#print CategoryTheory.Abelian.coimageImageComparison /-
 /-- The canonical map from the abelian coimage to the abelian image.
 In any abelian category this is an isomorphism.
 
@@ -112,7 +133,9 @@ def coimageImageComparison : Abelian.coimage f ⟶ Abelian.image f :=
     ext
     simp
 #align category_theory.abelian.coimage_image_comparison CategoryTheory.Abelian.coimageImageComparison
+-/
 
+#print CategoryTheory.Abelian.coimageImageComparison' /-
 /-- An alternative formulation of the canonical map from the abelian coimage to the abelian image.
 -/
 def coimageImageComparison' : Abelian.coimage f ⟶ Abelian.image f :=
@@ -121,18 +144,23 @@ def coimageImageComparison' : Abelian.coimage f ⟶ Abelian.image f :=
       ext
       simp)
 #align category_theory.abelian.coimage_image_comparison' CategoryTheory.Abelian.coimageImageComparison'
+-/
 
+#print CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison' /-
 theorem coimageImageComparison_eq_coimageImageComparison' :
     coimageImageComparison f = coimageImageComparison' f :=
   by
   ext
   simp [coimage_image_comparison, coimage_image_comparison']
 #align category_theory.abelian.coimage_image_comparison_eq_coimage_image_comparison' CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison'
+-/
 
+#print CategoryTheory.Abelian.coimage_image_factorisation /-
 @[simp, reassoc.1]
 theorem coimage_image_factorisation : coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f := by
   simp [coimage_image_comparison]
 #align category_theory.abelian.coimage_image_factorisation CategoryTheory.Abelian.coimage_image_factorisation
+-/
 
 end CategoryTheory.Abelian
 

Mathbin/CategoryTheory/Idempotents/Biproducts.lean

@@ -134,18 +134,18 @@ instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
       snd := P.complement.decompIdP
       inl := P.decompIdI
       inr := P.complement.decompIdI
-      inl_fst' := P.decomp_id.symm
-      inl_snd' :=
+      inl_fst := P.decomp_id.symm
+      inl_snd :=
         by
         simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp_f, hom_ext,
           quiver.hom.add_comm_group_zero_f, P.idem]
         erw [comp_id, sub_self]
-      inr_fst' :=
+      inr_fst :=
         by
         simp only [decomp_id_i_f, complement_p, decomp_id_p_f, sub_comp, comp_f, hom_ext,
           quiver.hom.add_comm_group_zero_f, P.idem]
         erw [id_comp, sub_self]
-      inr_snd' := P.complement.decomp_id.symm }
+      inr_snd := P.complement.decomp_id.symm }
     (by
       simp only [hom_ext, ← decomp_p, quiver.hom.add_comm_group_add_f, to_karoubi_map_f, id_eq,
         coe_p, complement_p, add_sub_cancel'_right])