feat: gcongr lemmas for Additive/Multiplicative (#18959)

From FLT

Co-authored-by: Javier Lopez-Contreras <[email protected]>

Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean

@@ -86,6 +86,11 @@ theorem toMul_le {a b : Additive α} : a.toMul ≤ b.toMul ↔ a ≤ b :=
 theorem toMul_lt {a b : Additive α} : a.toMul < b.toMul ↔ a < b :=
   Iff.rfl
 
+@[gcongr] alias ⟨_, toMul_mono⟩ := toMul_le
+@[gcongr] alias ⟨_, ofMul_mono⟩ := ofMul_le
+@[gcongr] alias ⟨_, toMul_strictMono⟩ := toMul_lt
+@[gcongr] alias ⟨_, foMul_strictMono⟩ := ofMul_lt
+
 end Additive
 
 namespace Multiplicative
@@ -108,4 +113,9 @@ theorem toAdd_le {a b : Multiplicative α} : a.toAdd ≤ b.toAdd ↔ a ≤ b :=
 theorem toAdd_lt {a b : Multiplicative α} : a.toAdd < b.toAdd ↔ a < b :=
   Iff.rfl
 
+@[gcongr] alias ⟨_, toAdd_mono⟩ := toAdd_le
+@[gcongr] alias ⟨_, ofAdd_mono⟩ := ofAdd_le
+@[gcongr] alias ⟨_, toAdd_strictMono⟩ := toAdd_lt
+@[gcongr] alias ⟨_, ofAdd_strictMono⟩ := ofAdd_lt
+
 end Multiplicative

Mathlib/MeasureTheory/OuterMeasure/Basic.lean

@@ -61,7 +61,7 @@ theorem measure_iUnion_le [Countable ι] (s : ι → Set α) : μ (⋃ i, s i) 
     μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
     _ ≤ ∑' i, μ (disjointed t i) :=
       OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)
-    _ ≤ ∑' i, μ (t i) := by gcongr; apply disjointed_subset
+    _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..
 
 theorem measure_biUnion_le {I : Set ι} (μ : F) (hI : I.Countable) (s : ι → Set α) :
     μ (⋃ i ∈ I, s i) ≤ ∑' i : I, μ (s i) := by