chore: no newline before aligns (#3735)

Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Apr 29, 2023 · aff74ff · aff74ff
1 parent 3894e48
commit aff74ff
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 16 deletions.
diff --git a/Mathlib/CategoryTheory/Limits/KanExtension.lean b/Mathlib/CategoryTheory/Limits/KanExtension.lean
@@ -56,7 +56,7 @@ attribute [local simp] StructuredArrow.proj
 abbrev diagram (F : S ⥤ D) (x : L) : StructuredArrow x ι ⥤ D :=
   StructuredArrow.proj x ι ⋙ F
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.diagram CategoryTheory.Ran.diagram
+#align category_theory.Ran.diagram CategoryTheory.Ran.diagram
 
 variable {ι}
 
@@ -76,7 +76,7 @@ def cone {F : S ⥤ D} {G : L ⥤ D} (x : L) (f : ι ⋙ G ⟶ F) : Cone (diagra
         have := f.naturality
         aesop_cat }
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.cone CategoryTheory.Ran.cone
+#align category_theory.Ran.cone CategoryTheory.Ran.cone
 
 variable (ι)
 
@@ -111,7 +111,7 @@ def loc (F : S ⥤ D) [h : ∀ x, HasLimit (diagram ι F x)] : L ⥤ D
     congr 1
     aesop_cat
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.loc CategoryTheory.Ran.loc
+#align category_theory.Ran.loc CategoryTheory.Ran.loc
 
 /-- An auxiliary definition used to define `Ran` and `Ran.adjunction`. -/
 @[simps]
@@ -156,7 +156,7 @@ def equiv (F : S ⥤ D) [h : ∀ x, HasLimit (diagram ι F x)] (G : L ⥤ D) :
     aesop_cat
   right_inv := by aesop_cat
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.equiv CategoryTheory.Ran.equiv
+#align category_theory.Ran.equiv CategoryTheory.Ran.equiv
 
 end Ran
 
@@ -172,7 +172,7 @@ def ran [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] : (S ⥤ D) ⥤ L ⥤
     dsimp [Ran.equiv]
     simp })
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran CategoryTheory.ran
+#align category_theory.Ran CategoryTheory.ran
 
 namespace Ran
 
@@ -183,7 +183,7 @@ def adjunction [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] :
     (whiskeringLeft _ _ D).obj ι ⊣ ran ι :=
   Adjunction.adjunctionOfEquivRight _ _
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.adjunction CategoryTheory.Ran.adjunction
+#align category_theory.Ran.adjunction CategoryTheory.Ran.adjunction
 
 theorem reflective [Full ι] [Faithful ι] [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] :
     IsIso (adjunction D ι).counit := by
@@ -200,7 +200,7 @@ theorem reflective [Full ι] [Faithful ι] [∀ X, HasLimitsOfShape (StructuredA
       ((limit.isLimit _).conePointUniqueUpToIso
         (limitOfDiagramInitial StructuredArrow.mkIdInitial _))
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Ran.reflective CategoryTheory.Ran.reflective
+#align category_theory.Ran.reflective CategoryTheory.Ran.reflective
 
 end Ran
 
@@ -212,7 +212,7 @@ attribute [local simp] CostructuredArrow.proj
 abbrev diagram (F : S ⥤ D) (x : L) : CostructuredArrow ι x ⥤ D :=
   CostructuredArrow.proj ι x ⋙ F
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.diagram CategoryTheory.Lan.diagram
+#align category_theory.Lan.diagram CategoryTheory.Lan.diagram
 
 variable {ι}
 
@@ -230,7 +230,7 @@ def cocone {F : S ⥤ D} {G : L ⥤ D} (x : L) (f : F ⟶ ι ⋙ G) : Cocone (di
         rw [← G.map_comp, ff]
         aesop_cat }
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.cocone CategoryTheory.Lan.cocone
+#align category_theory.Lan.cocone CategoryTheory.Lan.cocone
 
 variable (ι)
 
@@ -268,7 +268,7 @@ def loc (F : S ⥤ D) [I : ∀ x, HasColimit (diagram ι F x)] : L ⥤ D
     congr 1
     simp
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.loc CategoryTheory.Lan.loc
+#align category_theory.Lan.loc CategoryTheory.Lan.loc
 
 /-- An auxiliary definition used to define `Lan` and `Lan.adjunction`. -/
 @[simps]
@@ -325,7 +325,7 @@ def equiv (F : S ⥤ D) [I : ∀ x, HasColimit (diagram ι F x)] (G : L ⥤ D) :
     rfl
   right_inv := by aesop_cat
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.equiv CategoryTheory.Lan.equiv
+#align category_theory.Lan.equiv CategoryTheory.Lan.equiv
 
 end Lan
 
@@ -337,7 +337,7 @@ def lan [∀ X, HasColimitsOfShape (CostructuredArrow ι X) D] : (S ⥤ D) ⥤ L
     ext
     simp [Lan.equiv] })
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan CategoryTheory.lan
+#align category_theory.Lan CategoryTheory.lan
 
 namespace Lan
 
@@ -348,7 +348,7 @@ def adjunction [∀ X, HasColimitsOfShape (CostructuredArrow ι X) D] :
     lan ι ⊣ (whiskeringLeft _ _ D).obj ι :=
   Adjunction.adjunctionOfEquivLeft _ _
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.adjunction CategoryTheory.Lan.adjunction
+#align category_theory.Lan.adjunction CategoryTheory.Lan.adjunction
 
 theorem coreflective [Full ι] [Faithful ι] [∀ X, HasColimitsOfShape (CostructuredArrow ι X) D] :
     IsIso (adjunction D ι).unit := by
@@ -365,7 +365,7 @@ theorem coreflective [Full ι] [Faithful ι] [∀ X, HasColimitsOfShape (Costruc
       ((colimit.isColimit _).coconePointUniqueUpToIso
           (colimitOfDiagramTerminal CostructuredArrow.mkIdTerminal _)).symm
 set_option linter.uppercaseLean3 false in
-  #align category_theory.Lan.coreflective CategoryTheory.Lan.coreflective
+#align category_theory.Lan.coreflective CategoryTheory.Lan.coreflective
 
 end Lan
 

diff --git a/Mathlib/Data/Finset/Sym.lean b/Mathlib/Data/Finset/Sym.lean
@@ -254,7 +254,7 @@ def symInsertEquiv (h : a ∉ s) : (insert a s).sym n ≃ Σi : Fin (n + 1), s.s
       swap; exact Subtype.coe_injective
       refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)
       exacts[rfl, h ∘ mem_sym_iff.1 hm a]
- #align finset.sym_insert_equiv Finset.symInsertEquiv
+#align finset.sym_insert_equiv Finset.symInsertEquiv
 
 end Sym
 

diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -948,7 +948,7 @@ instance add_covariantClass_le : CovariantClass Ordinal.{u} Ordinal.{u} (· + ·
       | Sum.inr a, Sum.inr b, H =>
         let ⟨w, h⟩ := fi _ _ (Sum.lex_inr_inr.1 H)
         exact ⟨Sum.inr w, congr_arg Sum.inr h⟩
-  #align ordinal.add_covariant_class_le Ordinal.add_covariantClass_le
+#align ordinal.add_covariant_class_le Ordinal.add_covariantClass_le
 
 -- Porting note: Rewritten proof of elim, previous version was difficult to debug
 instance add_swap_covariantClass_le :