refactor: add gcongr tag to IsMeagre.mono (#32686)

Note that to add the `gcongr` attribute we are required to reorder the last two arguments of `IsMeagre.mono`.

Co-authored-by: Lara Toledano <lara_toledano@yahoo.fr>

Author: LTolDe

Mathlib/Topology/GDelta/Basic.lean

@@ -223,7 +223,8 @@ lemma IsMeagre.empty : IsMeagre (∅ : Set X) := by
   exact Filter.univ_mem
 
 /-- Subsets of meagre sets are meagre. -/
-lemma IsMeagre.mono {s t : Set X} (hs : IsMeagre s) (hts : t ⊆ s) : IsMeagre t :=
+@[gcongr]
+lemma IsMeagre.mono {s t : Set X} (hts : t ⊆ s) (hs : IsMeagre s) : IsMeagre t :=
   Filter.mem_of_superset hs (compl_subset_compl.mpr hts)
 
 /-- An intersection with a meagre set is meagre. -/