chore(TopCat/Limits/Cofiltered): golf (#9279)

leanprover-community · Dec 26, 2023 · 925559d · 925559d
1 parent 9d6b50d
commit 925559d
Showing 1 changed file with 4 additions and 8 deletions.
diff --git a/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean b/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
@@ -70,14 +70,10 @@ theorem isTopologicalBasis_cofiltered_limit (T : ∀ j, Set (Set (F.obj j)))
   · rintro ⟨j, V, hV, rfl⟩
     let U : ∀ i, Set (F.obj i) := fun i => if h : i = j then by rw [h]; exact V else Set.univ
     refine' ⟨U, {j}, _, _⟩
-    · rintro i h
-      rw [Finset.mem_singleton] at h
-      dsimp
-      rw [dif_pos h]
-      subst h
-      exact hV
-    · dsimp
-      simp
+    · simp only [Finset.mem_singleton]
+      rintro i rfl
+      simpa
+    · simp
   · rintro ⟨U, G, h1, h2⟩
     obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
     let g : ∀ (e) (_he : e ∈ G), j ⟶ e := fun _ he => (hj he).some