fix: add missing aligns to category files (#2320)

leanprover-community · Mar 4, 2023 · b556815 · b556815
1 parent 3636a40
commit b556815
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 0 deletions.
diff --git a/Mathlib/CategoryTheory/Bicategory/Basic.lean b/Mathlib/CategoryTheory/Bicategory/Basic.lean
@@ -129,6 +129,23 @@ class Bicategory (B : Type u) extends CategoryStruct.{v} B where
       = whiskerRight (rightUnitor f).hom g := by
     aesop_cat
 #align category_theory.bicategory CategoryTheory.Bicategory
+#align category_theory.bicategory.hom_category CategoryTheory.Bicategory.homCategory
+#align category_theory.bicategory.whisker_left CategoryTheory.Bicategory.whiskerLeft
+#align category_theory.bicategory.whisker_right CategoryTheory.Bicategory.whiskerRight
+#align category_theory.bicategory.left_unitor CategoryTheory.Bicategory.leftUnitor
+#align category_theory.bicategory.right_unitor CategoryTheory.Bicategory.rightUnitor
+#align category_theory.bicategory.whisker_left_id' CategoryTheory.Bicategory.whiskerLeft_id
+#align category_theory.bicategory.whisker_left_comp' CategoryTheory.Bicategory.whiskerLeft_comp
+#align category_theory.bicategory.id_whisker_left' CategoryTheory.Bicategory.id_whiskerLeft
+#align category_theory.bicategory.comp_whisker_left' CategoryTheory.Bicategory.comp_whiskerLeft
+#align category_theory.bicategory.id_whisker_right' CategoryTheory.Bicategory.id_whiskerRight
+#align category_theory.bicategory.comp_whisker_right' CategoryTheory.Bicategory.comp_whiskerRight
+#align category_theory.bicategory.whisker_right_id' CategoryTheory.Bicategory.whiskerRight_id
+#align category_theory.bicategory.whisker_right_comp' CategoryTheory.Bicategory.whiskerRight_comp
+#align category_theory.bicategory.whisker_assoc' CategoryTheory.Bicategory.whisker_assoc
+#align category_theory.bicategory.whisker_exchange' CategoryTheory.Bicategory.whisker_exchange
+#align category_theory.bicategory.pentagon' CategoryTheory.Bicategory.pentagon
+#align category_theory.bicategory.triangle' CategoryTheory.Bicategory.triangle
 
 namespace Bicategory
 

diff --git a/Mathlib/CategoryTheory/EpiMono.lean b/Mathlib/CategoryTheory/EpiMono.lean
@@ -63,6 +63,7 @@ class IsSplitMono {X Y : C} (f : X ⟶ Y) : Prop where
   /-- There is a splitting -/ 
   exists_splitMono : Nonempty (SplitMono f)
 #align category_theory.is_split_mono CategoryTheory.IsSplitMono
+#align category_theory.is_split_mono.exists_split_mono CategoryTheory.IsSplitMono.exists_splitMono
 
 /-- A constructor for `IsSplitMono f` taking a `SplitMono f` as an argument -/
 theorem IsSplitMono.mk' {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : IsSplitMono f :=
@@ -92,6 +93,7 @@ class IsSplitEpi {X Y : C} (f : X ⟶ Y) : Prop where
   /-- There is a splitting -/
   exists_splitEpi : Nonempty (SplitEpi f)
 #align category_theory.is_split_epi CategoryTheory.IsSplitEpi
+#align category_theory.is_split_epi.exists_split_epi CategoryTheory.IsSplitEpi.exists_splitEpi
 
 /-- A constructor for `IsSplitEpi f` taking a `SplitEpi f` as an argument -/
 theorem IsSplitEpi.mk' {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : IsSplitEpi f :=
@@ -223,12 +225,14 @@ class SplitMonoCategory where
   /-- All monos are split -/
   isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], IsSplitMono f
 #align category_theory.split_mono_category CategoryTheory.SplitMonoCategory
+#align category_theory.split_mono_category.is_split_mono_of_mono CategoryTheory.SplitMonoCategory.isSplitMono_of_mono
 
 /-- A split epi category is a category in which every epimorphism is split. -/
 class SplitEpiCategory where
   /-- All epis are split -/
   isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], IsSplitEpi f
 #align category_theory.split_epi_category CategoryTheory.SplitEpiCategory
+#align category_theory.split_epi_category.is_split_epi_of_epi CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi
 
 end
 

diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean
@@ -93,6 +93,9 @@ structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Categ
     ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) =
       𝟙 (functor.obj X) := by aesop_cat
 #align category_theory.equivalence CategoryTheory.Equivalence
+#align category_theory.equivalence.unit_iso CategoryTheory.Equivalence.unitIso
+#align category_theory.equivalence.counit_iso CategoryTheory.Equivalence.counitIso
+#align category_theory.equivalence.functor_unit_iso_comp CategoryTheory.Equivalence.functor_unitIso_comp
 
 /-- We infix the usual notation for an equivalence -/
 infixr:10 " ≌ " => Equivalence
@@ -496,6 +499,9 @@ class IsEquivalence (F : C ⥤ D) where mk' ::
         𝟙 (F.obj X) := by
     aesop_cat
 #align category_theory.is_equivalence CategoryTheory.IsEquivalence
+#align category_theory.is_equivalence.unit_iso CategoryTheory.IsEquivalence.unitIso
+#align category_theory.is_equivalence.counit_iso CategoryTheory.IsEquivalence.counitIso
+#align category_theory.is_equivalence.functor_unit_iso_comp CategoryTheory.IsEquivalence.functor_unitIso_comp
 
 attribute [reassoc (attr := simp)] IsEquivalence.functor_unitIso_comp