From 4874898f684980842bd8170f8975c997443b362f Mon Sep 17 00:00:00 2001
From: Suzuka Yu <109365723+Yu-Misaka@users.noreply.github.com>
Date: Sat, 5 Oct 2024 16:35:12 +0800
Subject: [PATCH] clean up

---
 FilteredRing/category.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

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