clean up

Blackfeather007 · Oct 5, 2024 · 4874898 · 4874898
1 parent ec9e77b
commit 4874898
Showing 1 changed file with 1 addition and 4 deletions.
diff --git 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