diff --git a/LeanCondensed/Projects/AB.lean b/LeanCondensed/Projects/AB.lean
index eff6576..21ee2af 100644
--- a/LeanCondensed/Projects/AB.lean
+++ b/LeanCondensed/Projects/AB.lean
@@ -36,7 +36,7 @@ lemma forall_exact_iff_functorEquivalence_exact (F : I ⥤ ShortComplex A) : (
 
 class HasExactLimitsOfShape : Prop where
   hasLimitsOfShape : HasLimitsOfShape I A := by infer_instance
-  exact_limit (F : I ⥤ ShortComplex A) :  (∀ i, (F.obj i).ShortExact) → (limit F).ShortExact
+  exact_limit (F : I ⥤ ShortComplex A) : (∀ i, (F.obj i).ShortExact) → (limit F).ShortExact
 
 attribute [instance] HasExactLimitsOfShape.hasLimitsOfShape