diff --git a/SimpleCounterexamples/BadInfinities.lean b/SimpleCounterexamples/BadInfinities.lean
index daf035a..23e27ac 100644
--- a/SimpleCounterexamples/BadInfinities.lean
+++ b/SimpleCounterexamples/BadInfinities.lean
@@ -7,7 +7,6 @@ theorem lt_irrefl_imp_no_infinity
   have hlt : inf < inf := h inf
   exact irrefl inf hlt
 
-
 theorem no_nat_infinity : ¬HasInfinity Nat :=
   lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl