chore(*): golf, mostly using gcongr (#12944)

Golf, mostly in `MeasureTheory` using `gcongr`.
Also add some missing `gcongr` lemmas.

Author: urkud

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -185,8 +185,7 @@ theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E)
       · rcases ((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_closedBall).1
             (Hs x hx.2) _ (half_pos <| half_pos ε0) with ⟨δ₁, δ₁0, hδ₁⟩
         filter_upwards [Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, δ₁0⟩] with δ hδ y₁ hy₁ y₂ hy₂
-        have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) :=
-          inter_subset_inter_left _ (closedBall_subset_closedBall hδ.2)
+        have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) := by gcongr; exact hδ.2
         rw [← dist_eq_norm]
         calc
           dist (f y₁) (f y₂) ≤ dist (f y₁) (f x) + dist (f y₂) (f x) := dist_triangle_right _ _ _

Mathlib/Data/Set/Accumulate.lean

@@ -42,6 +42,11 @@ theorem monotone_accumulate [Preorder α] : Monotone (Accumulate s) := fun _ _ h
   biUnion_subset_biUnion_left fun _ hz => le_trans hz hxy
 #align set.monotone_accumulate Set.monotone_accumulate
 
+@[gcongr]
+theorem accumulate_subset_accumulate [Preorder α] {x y} (h : x ≤ y) :
+    Accumulate s x ⊆ Accumulate s y :=
+  monotone_accumulate h
+
 theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y := by
   apply Subset.antisymm
   · exact iUnion₂_subset fun y hy => monotone_accumulate hy

Mathlib/Data/Set/Prod.lean

@@ -43,14 +43,17 @@ noncomputable instance decidableMemProd [DecidablePred (· ∈ s)] [DecidablePre
     DecidablePred (· ∈ s ×ˢ t) := fun _ => And.decidable
 #align set.decidable_mem_prod Set.decidableMemProd
 
+@[gcongr]
 theorem prod_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂ :=
   fun _ ⟨h₁, h₂⟩ => ⟨hs h₁, ht h₂⟩
 #align set.prod_mono Set.prod_mono
 
+@[gcongr]
 theorem prod_mono_left (hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t :=
   prod_mono hs Subset.rfl
 #align set.prod_mono_left Set.prod_mono_left
 
+@[gcongr]
 theorem prod_mono_right (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂ :=
   prod_mono Subset.rfl ht
 #align set.prod_mono_right Set.prod_mono_right

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -297,8 +297,8 @@ theorem pi_caratheodory :
   simp_rw [piPremeasure]
   refine' Finset.prod_add_prod_le' (Finset.mem_univ i) _ _ _
   · simp [image_inter_preimage, image_diff_preimage, measure_inter_add_diff _ hs, le_refl]
-  · rintro j - _; apply mono'; apply image_subset; apply inter_subset_left
-  · rintro j - _; apply mono'; apply image_subset; apply diff_subset
+  · rintro j - _; gcongr; apply inter_subset_left
+  · rintro j - _; gcongr; apply diff_subset
 #align measure_theory.measure.pi_caratheodory MeasureTheory.Measure.pi_caratheodory
 
 /-- `Measure.pi μ` is the finite product of the measures `{μ i | i : ι}`.

Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

@@ -349,15 +349,15 @@ do not need the sets to be measurable. -/
 @[simp]
 theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t := by
   apply le_antisymm
-  · set ST := toMeasurable μ s ×ˢ toMeasurable ν t
-    have hSTm : MeasurableSet ST :=
+  · set S := toMeasurable μ s
+    set T := toMeasurable ν t
+    have hSTm : MeasurableSet (S ×ˢ T) :=
       (measurableSet_toMeasurable _ _).prod (measurableSet_toMeasurable _ _)
     calc
-      μ.prod ν (s ×ˢ t) ≤ μ.prod ν ST :=
-        measure_mono <| Set.prod_mono (subset_toMeasurable _ _) (subset_toMeasurable _ _)
-      _ = μ (toMeasurable μ s) * ν (toMeasurable ν t) := by
+      μ.prod ν (s ×ˢ t) ≤ μ.prod ν (S ×ˢ T) := by gcongr <;> apply subset_toMeasurable
+      _ = μ S * ν T := by
         rw [prod_apply hSTm]
-        simp_rw [ST, mk_preimage_prod_right_eq_if, measure_if,
+        simp_rw [mk_preimage_prod_right_eq_if, measure_if,
           lintegral_indicator _ (measurableSet_toMeasurable _ _), lintegral_const,
           restrict_apply_univ, mul_comm]
       _ = μ s * ν t := by rw [measure_toMeasurable, measure_toMeasurable]
@@ -370,7 +370,7 @@ theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν
     set s' : Set α := { x | ν t ≤ f x }
     have hss' : s ⊆ s' := fun x hx => measure_mono fun y hy => hST <| mk_mem_prod hx hy
     calc
-      μ s * ν t ≤ μ s' * ν t := mul_le_mul_right' (measure_mono hss') _
+      μ s * ν t ≤ μ s' * ν t := by gcongr
       _ = ∫⁻ _ in s', ν t ∂μ := by rw [set_lintegral_const, mul_comm]
       _ ≤ ∫⁻ x in s', f x ∂μ := set_lintegral_mono measurable_const hfm fun x => id
       _ ≤ ∫⁻ x, f x ∂μ := lintegral_mono' restrict_le_self le_rfl
@@ -533,8 +533,7 @@ lemma set_prod_ae_eq {s s' : Set α} {t t' : Set β} (hs : s =ᵐ[μ] s') (ht :
 lemma measure_prod_compl_eq_zero {s : Set α} {t : Set β}
     (s_ae_univ : μ sᶜ = 0) (t_ae_univ : ν tᶜ = 0) :
     μ.prod ν (s ×ˢ t)ᶜ = 0 := by
-  rw [Set.compl_prod_eq_union]
-  apply le_antisymm ((measure_union_le _ _).trans _) (zero_le _)
+  rw [Set.compl_prod_eq_union, measure_union_null_iff]
   simp [s_ae_univ, t_ae_univ]
 
 lemma _root_.MeasureTheory.NullMeasurableSet.prod {s : Set α} {t : Set β}

Mathlib/MeasureTheory/Covering/Besicovitch.lean

@@ -141,6 +141,21 @@ structure Besicovitch.SatelliteConfig (α : Type*) [MetricSpace α] (N : ℕ) (
 #align besicovitch.satellite_config.hlast Besicovitch.SatelliteConfig.hlast
 #align besicovitch.satellite_config.inter Besicovitch.SatelliteConfig.inter
 
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq
+
+/-- Extension for the `positivity` tactic: `Besicovitch.SatelliteConfig.r`. -/
+@[positivity Besicovitch.SatelliteConfig.r _ _]
+def evalBesicovitchSatelliteConfigR : PositivityExt where eval {u α} _zα _pα e := do
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(@Besicovitch.SatelliteConfig.r $β $inst $N $τ $self $i) =>
+    assertInstancesCommute
+    return .positive q(Besicovitch.SatelliteConfig.rpos $self $i)
+  | _, _, _ => throwError "not Besicovitch.SatelliteConfig.r"
+
+end Mathlib.Meta.Positivity
+
 /-- A metric space has the Besicovitch covering property if there exist `N` and `τ > 1` such that
 there are no satellite configuration of parameter `τ` with `N+1` points. This is the condition that
 guarantees that the measurable Besicovitch covering theorem holds. It is satisfied by
@@ -650,8 +665,8 @@ theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMea
       μ o = 1 / (N + 1) * μ s + N / (N + 1) * μ s := by
         rw [μo, ← add_mul, ENNReal.div_add_div_same, add_comm, ENNReal.div_self, one_mul] <;> simp
       _ ≤ μ ((⋃ x ∈ w, closedBall (↑x) (r ↑x)) ∩ o) + N / (N + 1) * μ s := by
-        refine' add_le_add _ le_rfl
-        rw [div_eq_mul_inv, one_mul, mul_comm, ← div_eq_mul_inv]
+        gcongr
+        rw [one_div, mul_comm, ← div_eq_mul_inv]
         apply hw.le.trans (le_of_eq _)
         rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe,
           measure_biUnion_finset]
@@ -783,8 +798,7 @@ theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measur
         μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ ⋃ n : ℕ, (u n : Set (α × ℝ))), closedBall p.fst p.snd) ≤
           μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u n), closedBall p.fst p.snd) := by
       intro n
-      apply measure_mono
-      apply diff_subset_diff (Subset.refl _)
+      gcongr μ (s \ ?_)
       exact biUnion_subset_biUnion_left (subset_iUnion (fun i => (u i : Set (α × ℝ))) n)
     have B :
         ∀ n, μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u n), closedBall p.fst p.snd) ≤
@@ -1029,12 +1043,10 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit
             ∑ i : Fin N, ∑' x : ((↑) : s' → α) '' S i, μ (closedBall x (r x)) :=
         (add_le_add le_rfl (ENNReal.tsum_iUnion_le (fun x => μ (closedBall x (r x))) _))
       _ ≤ μ s + ε / 2 + ∑ i : Fin N, ε / 2 / N := by
-        refine' add_le_add A _
-        refine' Finset.sum_le_sum _
-        intro i _
-        exact B i
+        gcongr
+        apply B
       _ ≤ μ s + ε / 2 + ε / 2 := by
-        refine' add_le_add le_rfl _
+        gcongr
         simp only [Finset.card_fin, Finset.sum_const, nsmul_eq_mul, ENNReal.mul_div_le]
       _ = μ s + ε := by rw [add_assoc, ENNReal.add_halves]
 #align besicovitch.exists_closed_ball_covering_tsum_measure_le Besicovitch.exists_closedBall_covering_tsum_measure_le

Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

@@ -64,51 +64,20 @@ radius at `1`. -/
 def centerAndRescale : SatelliteConfig E N τ where
   c i := (a.r (last N))⁻¹ • (a.c i - a.c (last N))
   r i := (a.r (last N))⁻¹ * a.r i
-  rpos i := mul_pos (inv_pos.2 (a.rpos _)) (a.rpos _)
+  rpos i := by positivity
   h i j hij := by
-    rcases a.h hij with (H | H)
-    · left
-      constructor
-      · rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs,
-          abs_of_nonneg (inv_nonneg.2 (a.rpos _).le)]
-        refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-        rw [dist_eq_norm] at H
-        convert H.1 using 2
-        abel
-      · rw [← mul_assoc, mul_comm τ, mul_assoc]
-        refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-        exact H.2
-    · right
-      constructor
-      · rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs,
-          abs_of_nonneg (inv_nonneg.2 (a.rpos _).le)]
-        refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-        rw [dist_eq_norm] at H
-        convert H.1 using 2
-        abel
-      · rw [← mul_assoc, mul_comm τ, mul_assoc]
-        refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-        exact H.2
+    simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
+      Real.norm_of_nonneg]
+    rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right] <;> constructor <;> gcongr
   hlast i hi := by
-    have H := a.hlast i hi
-    constructor
-    · rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs,
-        abs_of_nonneg (inv_nonneg.2 (a.rpos _).le)]
-      refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-      rw [dist_eq_norm] at H
-      convert H.1 using 2
-      abel
-    · rw [← mul_assoc, mul_comm τ, mul_assoc]
-      refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-      exact H.2
+    simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
+      Real.norm_of_nonneg]
+    have ⟨H₁, H₂⟩ := a.hlast i hi
+    constructor <;> gcongr
   inter i hi := by
-    have H := a.inter i hi
-    rw [dist_eq_norm, ← smul_sub, norm_smul, Real.norm_eq_abs,
-      abs_of_nonneg (inv_nonneg.2 (a.rpos _).le), ← mul_add]
-    refine' mul_le_mul_of_nonneg_left _ (inv_nonneg.2 (a.rpos _).le)
-    rw [dist_eq_norm] at H
-    convert H using 2
-    abel
+    simp (disch := positivity) only [dist_smul₀, ← mul_add, dist_sub_right, Real.norm_of_nonneg]
+    gcongr
+    exact a.inter i hi
 #align besicovitch.satellite_config.center_and_rescale Besicovitch.SatelliteConfig.centerAndRescale
 
 theorem centerAndRescale_center : a.centerAndRescale.c (last N) = 0 := by
@@ -362,7 +331,7 @@ theorem exists_normalized_aux1 {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ)
   have τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ
   have I : (1 - δ / 4) * τ ≤ 1 :=
     calc
-      (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := mul_le_mul_of_nonneg_left hδ1 D
+      (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := by gcongr
       _ = (1 : ℝ) - δ ^ 2 / 16 := by ring
       _ ≤ 1 := by linarith only [sq_nonneg δ]
   have J : 1 - δ ≤ 1 - δ / 4 := by linarith only [δnonneg]
@@ -396,7 +365,6 @@ theorem exists_normalized_aux2 {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ)
     simpa only [dist_eq_norm] using a.h
   have δnonneg : 0 ≤ δ := by linarith only [hτ, hδ1]
   have D : 0 ≤ 1 - δ / 4 := by linarith only [hδ2]
-  have τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ
   have hcrj : ‖a.c j‖ ≤ a.r j + 1 := by simpa only [lastc, lastr, dist_zero_right] using a.inter' j
   have I : a.r i ≤ 2 := by
     rcases lt_or_le i (last N) with (H | H)
@@ -407,25 +375,25 @@ theorem exists_normalized_aux2 {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ)
       exact one_le_two
   have J : (1 - δ / 4) * τ ≤ 1 :=
     calc
-      (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := mul_le_mul_of_nonneg_left hδ1 D
+      (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := by gcongr
       _ = (1 : ℝ) - δ ^ 2 / 16 := by ring
       _ ≤ 1 := by linarith only [sq_nonneg δ]
   have A : a.r j - δ ≤ ‖a.c i - a.c j‖ := by
     rcases ah inej.symm with (H | H); · rw [norm_sub_rev]; linarith [H.1]
     have C : a.r j ≤ 4 :=
       calc
         a.r j ≤ τ * a.r i := H.2
-        _ ≤ τ * 2 := mul_le_mul_of_nonneg_left I τpos.le
-        _ ≤ 5 / 4 * 2 := (mul_le_mul_of_nonneg_right (by linarith only [hδ1, hδ2]) zero_le_two)
+        _ ≤ τ * 2 := by gcongr
+        _ ≤ 5 / 4 * 2 := by gcongr; linarith only [hδ1, hδ2]
         _ ≤ 4 := by norm_num
     calc
       a.r j - δ ≤ a.r j - a.r j / 4 * δ := by
-        refine' sub_le_sub le_rfl _
+        gcongr _ - ?_
         refine' mul_le_of_le_one_left δnonneg _
         linarith only [C]
       _ = (1 - δ / 4) * a.r j := by ring
       _ ≤ (1 - δ / 4) * (τ * a.r i) := mul_le_mul_of_nonneg_left H.2 D
-      _ ≤ 1 * a.r i := by rw [← mul_assoc]; apply mul_le_mul_of_nonneg_right J (a.rpos _).le
+      _ ≤ 1 * a.r i := by rw [← mul_assoc]; gcongr
       _ ≤ ‖a.c i - a.c j‖ := by rw [one_mul]; exact H.1
   set d := (2 / ‖a.c j‖) • a.c j with hd
   have : a.r j - δ ≤ ‖a.c i - d‖ + (a.r j - 1) :=

Mathlib/MeasureTheory/Covering/Vitali.lean

@@ -150,7 +150,7 @@ theorem exists_disjoint_subfamily_covering_enlargment (B : ι → Set α) (t : S
         calc
           δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
           _ = τ * (m / τ) := by field_simp [(zero_lt_one.trans hτ).ne']
-          _ ≤ τ * δ b := mul_le_mul_of_nonneg_left ha' (zero_le_one.trans hτ.le)
+          _ ≤ τ * δ b := by gcongr
       · rw [← not_disjoint_iff_nonempty_inter] at hcb
         exact (hcb (H _ H')).elim
 #align vitali.exists_disjoint_subfamily_covering_enlargment Vitali.exists_disjoint_subfamily_covering_enlargment
@@ -386,7 +386,7 @@ theorem exists_disjoint_covering_ae [MetricSpace α] [MeasurableSpace α] [Opens
     _ ≤ ∑' a : { a // a ∉ w }, μ (closedBall (c a) (3 * r a)) := measure_iUnion_le _
     _ ≤ ∑' a : { a // a ∉ w }, C * μ (B a) := (ENNReal.tsum_le_tsum fun a => μB a (ut (vu a.1.2)))
     _ = C * ∑' a : { a // a ∉ w }, μ (B a) := ENNReal.tsum_mul_left
-    _ ≤ C * (ε / C) := mul_le_mul_left' hw.le _
+    _ ≤ C * (ε / C) := by gcongr
     _ ≤ ε := ENNReal.mul_div_le
 #align vitali.exists_disjoint_covering_ae Vitali.exists_disjoint_covering_ae
 
@@ -418,10 +418,11 @@ protected def vitaliFamily [MetricSpace α] [MeasurableSpace α] [OpensMeasurabl
       intro x xs ε εpos
       rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩
       rcases fsubset x xs ha with ⟨a_closed, a_int, ⟨r, ar, μr⟩⟩
-      refine' ⟨⟨min r ε, x, a⟩, ⟨_, _, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
+      refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
       · rcases min_cases r ε with (h' | h') <;> rwa [h'.1]
-      · apply le_trans (measure_mono (closedBall_subset_closedBall _)) μr
-        exact mul_le_mul_of_nonneg_left (min_le_left _ _) zero_le_three
+      · apply le_trans ?_ μr
+        gcongr
+        apply min_le_left
     rcases exists_disjoint_covering_ae μ s t C (fun p => p.1) (fun p => p.2.1) (fun p => p.2.2)
         (fun p hp => hp.1) (fun p hp => hp.2.1) (fun p hp => hp.2.2.1) (fun p hp => hp.2.2.2.1) A
       with ⟨t', t't, _, t'_disj, μt'⟩

Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

@@ -110,11 +110,9 @@ theorem hahn_decomposition [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     · intro n (hmn : m ≤ n) ih
       have : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)) := by
         calc
-          γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) ≤
+          γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) =
               γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1))) := by
-            refine' add_le_add_left (add_le_add_left _ _) γ
-            simp only [pow_add, pow_one, le_sub_iff_add_le]
-            linarith
+            rw [pow_succ, mul_one_div, _root_.sub_half]
           _ = γ - (1 / 2) ^ (n + 1) + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n) := by
             simp only [sub_eq_add_neg]; abel
           _ ≤ d (e (n + 1)) + d (f m n) := add_le_add (le_of_lt <| he₂ _) ih
@@ -126,7 +124,6 @@ theorem hahn_decomposition [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
             · exact (he₁ _).union (hf _ _)
             · exact he₁ _
           _ ≤ γ + d (f m (n + 1)) := add_le_add_right (d_le_γ _ <| (he₁ _).union (hf _ _)) _
-
       exact (add_le_add_iff_left γ).1 this
   let s := ⋃ m, ⋂ n, f m n
   have γ_le_d_s : γ ≤ d s := by
@@ -169,7 +166,7 @@ theorem hahn_decomposition [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     have : d t ≤ 0 :=
       (add_le_add_iff_left γ).1 <|
         calc
-          γ + d t ≤ d s + d t := add_le_add γ_le_d_s le_rfl
+          γ + d t ≤ d s + d t := by gcongr
           _ = d (s ∪ t) := by
             rw [d_split _ _ (hs.union ht) ht, union_diff_right, union_inter_cancel_right,
               (subset_compl_iff_disjoint_left.1 hts).sdiff_eq_left]

Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

@@ -65,12 +65,11 @@ theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type
       μ t ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u' p ∩ v p q) := by
         refine (measure_iUnion_le _).trans ?_
         refine ENNReal.tsum_le_tsum fun p => ?_
-        refine @measure_iUnion_le _ _ _ _ ?_ _
-        exact (s_count.mono (inter_subset_left _ _)).to_subtype
+        haveI := (s_count.mono (inter_subset_left _ (Ioi ↑p))).to_subtype
+        apply measure_iUnion_le
       _ ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u p q ∩ v p q) := by
-        refine ENNReal.tsum_le_tsum fun p => ?_
-        refine ENNReal.tsum_le_tsum fun q => measure_mono ?_
-        exact inter_subset_inter_left _ (biInter_subset_of_mem q.2)
+        gcongr with p q
+        exact biInter_subset_of_mem q.2
       _ = ∑' (p : s) (_ : ↥(s ∩ Ioi p)), (0 : ℝ≥0∞) := by
         congr
         ext1 p