diff --git a/FilteredRing/category.lean b/FilteredRing/category.lean
index d652e13..6c6cce3 100644
--- a/FilteredRing/category.lean
+++ b/FilteredRing/category.lean
@@ -24,10 +24,7 @@ instance : Category (FilModCat R F) where
     rename_i X Y Z
     have aux1 := f.2 i
     have aux2 := g.2 i
-    suffices g.1 '' (f.1 '' (X.fil i)) ≤ (Z.fil i) from by
-      simp_all only [Set.le_eq_subset, Set.image_subset_iff, LinearMap.coe_comp, Function.comp_apply]
-      exact this
-    simp_all only [Set.le_eq_subset, Set.image_subset_iff]
+    simp_all only [Set.le_eq_subset, Set.image_subset_iff, LinearMap.coe_comp, Function.comp_apply]
     exact fun _ hx ↦ aux2 <| aux1 hx⟩
   id_comp _ := rfl
   comp_id _ := rfl