chore: replace mono by gcongr (#23968)

grunweg · grunweg · commit 446b459fb17e · 2025-04-17T14:45:00.000Z
gcongr is more maintained, and slightly faster here.




Co-authored-by: grunweg &lt;rothgami@math.hu-berlin.de&gt;
diff --git a/Mathlib/Dynamics/OmegaLimit.lean b/Mathlib/Dynamics/OmegaLimit.lean
@@ -227,7 +227,8 @@ theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit
     apply Subset.trans hg₃
     simp only [j, iUnion_subset_iff, compl_subset_compl]
     intros u hu
-    mono
+    unfold w
+    gcongr
     refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
     all_goals exact Subset.rfl
   have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ := by
