Apply suggestions from code review

dagurtomas · Jun 14, 2024 · 0909b46 · 0909b46
1 parent 4fa05f4
commit 0909b46
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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