chore: reduce use of mono in favour of gcongr (#13881)

... as was discussed on zulip the other day; I cannot find the link quickly.
After this PR, a handful of uses remain which are harder to remove: [this branch](https://github.com/leanprover-community/mathlib4/compare/MR-mono-gcongr) comments them all

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -528,8 +528,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
     have : (ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹ :=
       IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv stream_nth_eq succ_nth_stream_eq
     have : 0 ≤ conts.b := le_of_lt zero_lt_conts_b
-    -- Porting note: was `mono`
-    refine mul_le_mul_of_nonneg_right ?_ ?_ <;> assumption
+    gcongr; exact this
 #align generalized_continued_fraction.abs_sub_convergents_le GeneralizedContinuedFraction.abs_sub_convergents_le
 
 /-- Shows that `|v - Aₙ / Bₙ| ≤ 1 / (bₙ * Bₙ * Bₙ)`. This bound is worse than the one shown in

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -11,7 +11,6 @@ import Mathlib.LinearAlgebra.Eigenspace.Basic
 import Mathlib.Order.Filter.AtTopBot
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Nilpotent.Lemmas
-import Mathlib.Tactic.Monotonicity
 
 #align_import algebra.lie.nilpotent from "leanprover-community/mathlib"@"6b0169218d01f2837d79ea2784882009a0da1aa1"
 
@@ -481,12 +480,12 @@ theorem ucs_add (k l : ℕ) : N.ucs (k + l) = (N.ucs l).ucs k :=
   Function.iterate_add_apply normalizer k l N
 #align lie_submodule.ucs_add LieSubmodule.ucs_add
 
-@[mono]
+@[gcongr, mono]
 theorem ucs_mono (k : ℕ) (h : N₁ ≤ N₂) : N₁.ucs k ≤ N₂.ucs k := by
   induction' k with k ih
   · simpa
   simp only [ucs_succ]
-  mono
+  gcongr
 #align lie_submodule.ucs_mono LieSubmodule.ucs_mono
 
 theorem ucs_eq_self_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) : N₁.ucs k = N₁ := by
@@ -503,7 +502,7 @@ An important instance of this situation arises from a Cartan subalgebra `H ⊆ L
 theorem ucs_le_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) :
     (⊥ : LieSubmodule R L M).ucs k ≤ N₁ := by
   rw [← ucs_eq_self_of_normalizer_eq_self h k]
-  mono
+  gcongr
   simp
 #align lie_submodule.ucs_le_of_normalizer_eq_self LieSubmodule.ucs_le_of_normalizer_eq_self
 

Mathlib/Algebra/Lie/Normalizer.lean

@@ -71,11 +71,11 @@ theorem normalizer_inf : (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.n
   ext; simp [← forall_and]
 #align lie_submodule.normalizer_inf LieSubmodule.normalizer_inf
 
-@[mono]
+@[gcongr, mono]
 theorem normalizer_mono (h : N₁ ≤ N₂) : normalizer N₁ ≤ normalizer N₂ := by
   intro m hm
   rw [mem_normalizer] at hm ⊢
-  exact fun x => h (hm x)
+  exact fun x ↦ h (hm x)
 
 theorem monotone_normalizer : Monotone (normalizer : LieSubmodule R L M → LieSubmodule R L M) :=
   fun _ _ ↦ normalizer_mono

Mathlib/Analysis/Calculus/FDeriv/Extend.lean

@@ -29,8 +29,6 @@ open Filter Set Metric ContinuousLinearMap
 
 open scoped Topology
 
-attribute [local mono] Set.prod_mono
-
 /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
 derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
 with derivative `f'`. -/
@@ -87,7 +85,7 @@ theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : Set E} {x :
     refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key
     all_goals
       -- common start for both continuity proofs
-      have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by mono <;> exact inter_subset_right
+      have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by gcongr <;> exact inter_subset_right
       obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by
         simpa [closure_prod_eq] using closure_mono this uv_in
       apply ContinuousWithinAt.mono _ this

Mathlib/Analysis/Convex/Hull.lean

@@ -70,7 +70,7 @@ theorem Convex.convexHull_subset_iff (ht : Convex 𝕜 t) : convexHull 𝕜 s 
   (show (convexHull 𝕜).IsClosed t from ht).closure_le_iff
 #align convex.convex_hull_subset_iff Convex.convexHull_subset_iff
 
-@[mono]
+@[mono, gcongr]
 theorem convexHull_mono (hst : s ⊆ t) : convexHull 𝕜 s ⊆ convexHull 𝕜 t :=
   (convexHull 𝕜).monotone hst
 #align convex_hull_mono convexHull_mono

Mathlib/Analysis/NormedSpace/AddTorsorBases.lean

@@ -147,8 +147,7 @@ theorem interior_convexHull_nonempty_iff_affineSpan_eq_top [FiniteDimensional 
   obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
   suffices (interior (convexHull ℝ (range b))).Nonempty by
     rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
-    refine this.mono ?_
-    mono*
+    refine this.mono (by gcongr)
   lift t to Finset V using b.finite_set
   exact ⟨_, b.centroid_mem_interior_convexHull⟩
 #align interior_convex_hull_nonempty_iff_affine_span_eq_top interior_convexHull_nonempty_iff_affineSpan_eq_top

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -824,12 +824,7 @@ theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n /
     ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
       rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
         norm_div, Real.norm_natCast, Nat.cast_succ]
-    _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ :=
-      -- Porting note: this was `by mono* with 0 ≤ ‖x ^ n / (n !)‖, 0 ≤ ‖x‖ <;> apply norm_nonneg`
-      -- but we can't wait on `mono`.
-      mul_le_mul_of_nonneg_right
-        (div_le_div (norm_nonneg x) (le_refl ‖x‖) A (add_le_add (mono_cast hn) (le_refl 1)))
-        (norm_nonneg (x ^ n / n !))
+    _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr
 #align real.summable_pow_div_factorial Real.summable_pow_div_factorial
 
 theorem Real.tendsto_pow_div_factorial_atTop (x : ℝ) :

Mathlib/Data/Nat/Totient.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.CharP.Two
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Periodic
 import Mathlib.Data.ZMod.Basic
-import Mathlib.Tactic.Monotonicity
 
 #align_import data.nat.totient from "leanprover-community/mathlib"@"5cc2dfdd3e92f340411acea4427d701dc7ed26f8"
 
@@ -88,10 +87,7 @@ theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
   · rw [← filter_coprime_Ico_eq_totient a k]
     simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos),
       Nat.zero_eq, zero_add]
-    -- Porting note: below line was `mono`
-    refine Finset.card_mono ?_
-    refine monotone_filter_left a.Coprime ?_
-    simp only [Finset.le_eq_subset]
+    gcongr
     exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k)
   simp only [mul_succ]
   simp_rw [← add_assoc] at ih ⊢

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.Order.Iterate
 import Mathlib.Order.SemiconjSup
-import Mathlib.Tactic.Monotonicity
 import Mathlib.Topology.Order.MonotoneContinuity
 
 #align_import dynamics.circle.rotation_number.translation_number from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"

Mathlib/NumberTheory/PellMatiyasevic.lean

@@ -8,7 +8,6 @@ import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Star.Unitary
 import Mathlib.Data.Nat.ModEq
 import Mathlib.NumberTheory.Zsqrtd.Basic
-import Mathlib.Tactic.Monotonicity
 
 #align_import number_theory.pell_matiyasevic from "leanprover-community/mathlib"@"795b501869b9fa7aa716d5fdadd00c03f983a605"
 
@@ -937,7 +936,7 @@ theorem eq_pow_of_pell_lem {a y k : ℕ} (hy0 : y ≠ 0) (hk0 : k ≠ 0) (hyk :
       exact lt_of_le_of_lt (Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)) hya
     _ ≤ (a : ℤ) ^ 2 - (a - y : ℤ) ^ 2 - 1 := by
       have := hya.le
-      mono * <;> norm_cast <;> simp [Nat.zero_le, Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)]
+      gcongr <;> norm_cast <;> omega
     _ = 2 * a * y - y * y - 1 := by ring
 #align pell.eq_pow_of_pell_lem Pell.eq_pow_of_pell_lem
 

Mathlib/Topology/MetricSpace/Algebra.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Tactic.Monotonicity
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.MetricSpace.Lipschitz
 
@@ -164,7 +163,7 @@ instance (priority := 100) BoundedSMul.continuousSMul : ContinuousSMul α β whe
         add_le_add (dist_pair_smul _ _ _) (dist_smul_pair _ _ _)
       _ ≤ δ * (δ + dist b 0) + dist a 0 * δ := by
           have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
-          mono* <;> apply_rules [dist_nonneg, le_of_lt]
+          gcongr
       _ < ε := hδε
 #align has_bounded_smul.has_continuous_smul BoundedSMul.continuousSMul
 

Mathlib/Topology/UniformSpace/Basic.lean

@@ -165,7 +165,7 @@ theorem Monotone.compRel [Preorder β] {f g : β → Set (α × α)} (hf : Monot
     Monotone fun x => f x ○ g x := fun _ _ h _ ⟨z, h₁, h₂⟩ => ⟨z, hf h h₁, hg h h₂⟩
 #align monotone.comp_rel Monotone.compRel
 
-@[mono]
+@[mono, gcongr]
 theorem compRel_mono {f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : f ○ g ⊆ h ○ k :=
   fun _ ⟨z, h, h'⟩ => ⟨z, h₁ h, h₂ h'⟩
 #align comp_rel_mono compRel_mono
@@ -609,7 +609,7 @@ theorem comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α)
   use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
   have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
   calc symmetrizeRel w ○ symmetrizeRel w
-    _ ⊆ w ○ w := by mono
+    _ ⊆ w ○ w := by gcongr
     _ ⊆ s     := w_sub
 #align comp_symm_mem_uniformity_sets comp_symm_mem_uniformity_sets