chore: golf using filter_upwards (#11208)

This is presumably not exhaustive, but covers about a hundred instances.

Style opinions (e.g., why a particular change is great/not a good idea) are very welcome; I'm still forming my own.

Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

@@ -123,13 +123,12 @@ theorem ae_convolution_tendsto_right_of_locallyIntegrable
   have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
   simp only [Function.comp] at this
   apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (FiniteDimensional.finrank ℝ G)) this
-  · apply eventually_of_forall (fun i ↦ ?_)
-    apply hg.integrableOn_isCompact
-    exact isCompact_closedBall _ _
+  · filter_upwards with i using
+      hg.integrableOn_isCompact (isCompact_closedBall _ _)
   · apply tendsto_const_nhds.congr (fun i ↦ ?_)
     rw [← integral_neg_eq_self]
     simp only [sub_neg_eq_add, integral_add_left_eq_self, integral_normed]
-  · apply eventually_of_forall (fun i ↦ ?_)
+  · filter_upwards with i
     change support ((ContDiffBump.normed (φ i) μ) ∘ (fun y ↦ x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
     simp only [support_comp_eq_preimage, support_normed_eq]
     intro x hx

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -356,9 +356,9 @@ def y (D : ℝ) : E → ℝ :=
 
 theorem y_neg (D : ℝ) (x : E) : y D (-x) = y D x := by
   apply convolution_neg_of_neg_eq
-  · apply eventually_of_forall fun x => _
+  · filter_upwards with x
     simp only [w_def, Real.rpow_nat_cast, mul_inv_rev, smul_neg, u_neg, smul_eq_mul, forall_const]
-  · apply eventually_of_forall fun x => _
+  · filter_upwards with x
     simp only [φ, indicator, mem_closedBall, dist_zero_right, norm_neg, forall_const]
 #align exists_cont_diff_bump_base.Y_neg ExistsContDiffBumpBase.y_neg
 

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -99,14 +99,14 @@ theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul
     Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
       (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) := by
   apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)
-  · apply eventually_of_forall (fun t ↦ ?_)
+  · filter_upwards with t
     apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
     apply aestronglyMeasurable_const.smul
     apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
     apply AEMeasurable.aestronglyMeasurable
     exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)
   · filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)
-    apply eventually_of_forall (fun x ↦ ?_)
+    filter_upwards with x
     calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
       = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
     _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
@@ -124,15 +124,15 @@ theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul'
   have K_compact : IsCompact K := IsCompact.cthickening h'f
   apply tendsto_integral_filter_of_dominated_convergence
       (K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖))
-  · apply eventually_of_forall (fun t ↦ ?_)
+  · filter_upwards with t
     apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
     apply aestronglyMeasurable_const.smul
     apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
     apply AEMeasurable.aestronglyMeasurable
     exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)
   · filter_upwards [Ioc_mem_nhdsWithin_Ioi' zero_lt_one] with t ht
     have t_pos : 0 < t := ht.1
-    apply eventually_of_forall (fun x ↦ ?_)
+    filter_upwards with x
     by_cases hx : x ∈ K
     · calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
         = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, t_pos.le]

Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

@@ -189,10 +189,8 @@ theorem uniformCauchySeqOn_ball_of_fderiv {r : ℝ} (hf' : UniformCauchySeqOn f'
         (l ×ˢ l) (Metric.ball x r) by
     have := this.1.add this.2
     rw [add_zero] at this
-    refine' this.congr _
-    apply eventually_of_forall
-    intro n z _
-    simp
+    refine this.congr ?_
+    filter_upwards with n z _ using (by simp)
   constructor
   · -- This inequality follows from the mean value theorem
     rw [Metric.tendstoUniformlyOn_iff] at hf' ⊢

Mathlib/Analysis/Convolution.lean

@@ -227,7 +227,7 @@ theorem BddAbove.convolutionExistsAt' {x₀ : G} {s : Set G}
   set s' := (fun t => -t + x₀) ⁻¹' s
   have : ∀ᵐ t : G ∂μ.restrict s,
       ‖L (f t) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i : s', ‖g i‖) t := by
-    refine' eventually_of_forall _
+    filter_upwards
     refine' le_indicator (fun t ht => _) fun t ht => _
     · apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
       refine' (le_ciSup_set hbg <| mem_preimage.mpr _)
@@ -680,7 +680,7 @@ theorem BddAbove.continuous_convolution_right_of_integrable
     Continuous (f ⋆[L, μ] g) := by
   refine' continuous_iff_continuousAt.mpr fun x₀ => _
   have : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t : G ∂μ, ‖L (f t) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖ := by
-    refine' eventually_of_forall fun x => eventually_of_forall fun t => _
+    filter_upwards with x; filter_upwards with t
     apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl, le_ciSup hbg (x - t)]
   refine' continuousAt_of_dominated _ this _ _
   · exact eventually_of_forall fun x =>
@@ -1051,7 +1051,7 @@ theorem HasCompactSupport.hasFDerivAt_convolution_right (hcg : HasCompactSupport
   -- `refine' hasFDerivAt_integral_of_dominated_of_fderiv_le zero_lt_one h1 _ (h2 x₀) _ _ _`
   -- but it failed; surprisingly, `apply` works
   apply hasFDerivAt_integral_of_dominated_of_fderiv_le zero_lt_one h1 _ (h2 x₀)
-  · refine' eventually_of_forall fun t x hx =>
+  · filter_upwards with t x hx using
       (hcg.fderiv 𝕜).convolution_integrand_bound_right L' (hg.continuous_fderiv le_rfl)
         (ball_subset_closedBall hx)
   · rw [integrable_indicator_iff hK'.measurableSet]
@@ -1208,8 +1208,7 @@ theorem hasFDerivAt_convolution_right_with_param {g : P → G → E'} {s : Set P
   let bound : G → ℝ := indicator U fun t => ‖(L.precompR (P × G))‖ * ‖f t‖ * C
   have I4 : ∀ᵐ a : G ∂μ, ∀ x : P × G, dist x q₀ < δ →
       ‖L.precompR (P × G) (f a) (g' (x.fst, x.snd - a))‖ ≤ bound a := by
-    apply eventually_of_forall
-    intro a x hx
+    filter_upwards with a x hx
     rw [Prod.dist_eq, dist_eq_norm, dist_eq_norm] at hx
     have : (-tsupport fun a => g' (x.1, a)) + ball q₀.2 δ ⊆ U := by
       apply Subset.trans _ hδ
@@ -1232,8 +1231,7 @@ theorem hasFDerivAt_convolution_right_with_param {g : P → G → E'} {s : Set P
   have I6 : ∀ᵐ a : G ∂μ, ∀ x : P × G, dist x q₀ < δ →
       HasFDerivAt (fun x : P × G => L (f a) (g x.1 (x.2 - a)))
         ((L (f a)).comp (g' (x.fst, x.snd - a))) x := by
-    apply eventually_of_forall
-    intro a x hx
+    filter_upwards with a x hx
     apply (L _).hasFDerivAt.comp x
     have N : s ×ˢ univ ∈ 𝓝 (x.1, x.2 - a) := by
       apply A'

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -77,7 +77,7 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
       exact (hf.integrableOn_isCompact K_compact).norm
     have C : ∀ n, ∀ᵐ x ∂μ, ‖g n x • f x‖ ≤ bound x := by
       intro n
-      apply eventually_of_forall (fun x ↦ ?_)
+      filter_upwards with x
       rw [norm_smul]
       refine le_indicator_apply (fun _ ↦ ?_) (fun hxK ↦ ?_)
       · have : ‖g n x‖ ≤ 1 := by
@@ -88,7 +88,7 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
       · have : g n x = 0 := by rw [← nmem_support, g_supp]; contrapose! hxK; exact vK n hxK
         simp [this]
     have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) := by
-      apply eventually_of_forall (fun x ↦ ?_)
+      filter_upwards with x
       by_cases hxs : x ∈ s
       · have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
         simp [this, indicator_of_mem hxs f]

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -106,7 +106,7 @@ theorem hasFDerivAt_fourier [CompleteSpace E] [MeasurableSpace V] [BorelSpace V]
         L.continuous.aestronglyMeasurable.prod_mk hf.1
       apply aux0.comp_aestronglyMeasurable aux1
   have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
-    refine ae_of_all _ (fun v w' _ ↦ ?_)
+    filter_upwards with v w' _
     exact norm_fderiv_fourier_transform_integrand_right_le L f v w'
   have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
   have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=

Mathlib/Analysis/Fourier/Inversion.lean

@@ -51,14 +51,14 @@ lemma tendsto_integral_cexp_sq_smul (hf : Integrable f) :
     Tendsto (fun (c : ℝ) ↦ (∫ v : V, cexp (- c⁻¹ * ‖v‖^2) • f v))
       atTop (𝓝 (∫ v : V, f v)) := by
   apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
-  · apply eventually_of_forall (fun v ↦ ?_)
+  · filter_upwards with v
     nth_rewrite 2 [show f v = cexp (- (0 : ℝ) * ‖v‖^2) • f v by simp]
     apply (Tendsto.cexp _).smul_const
     exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _
-  · apply eventually_of_forall (fun c ↦ ?_)
-    exact AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by continuity)) hf.1
+  · filter_upwards with c using
+      AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by continuity)) hf.1
   · filter_upwards [Ici_mem_atTop (0 : ℝ)] with c (hc : 0 ≤ c)
-    apply eventually_of_forall (fun v ↦ ?_)
+    filter_upwards with v
     simp only [ofReal_inv, neg_mul, norm_smul, Complex.norm_eq_abs]
     norm_cast
     conv_rhs => rw [← one_mul (‖f v‖)]

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -105,8 +105,8 @@ theorem GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) :
     exact ContinuousAt.comp this continuous_ofReal.continuousAt
   · rw [← hasFiniteIntegral_norm_iff]
     refine' HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 _
-    refine' (ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ fun x hx => _)
-    dsimp only
+    apply (ae_restrict_iff' measurableSet_Ioi).mpr
+    filter_upwards with x hx
     rw [norm_eq_abs, map_mul, abs_of_nonneg <| le_of_lt <| exp_pos <| -x,
       abs_cpow_eq_rpow_re_of_pos hx _]
     simp
@@ -195,7 +195,7 @@ private theorem Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y
   refine' (((Real.GammaIntegral_convergent hs).mono_set
     Ioc_subset_Ioi_self).hasFiniteIntegral.congr _).const_mul _
   rw [EventuallyEq, ae_restrict_iff']
-  · apply ae_of_all; intro x hx
+  · filter_upwards with x hx
     rw [abs_of_nonneg (exp_pos _).le, abs_cpow_eq_rpow_re_of_pos hx.1]
     simp
   · exact measurableSet_Ioc

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -313,7 +313,7 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
     intro x hx
     apply Tendsto.congr'
     show ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
-    · refine' Eventually.mp (eventually_ge_atTop ⌈x⌉₊) (eventually_of_forall fun n hn => _)
+    · filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn
       rw [Nat.ceil_le] at hn
       dsimp only [f]
       rw [indicator_of_mem]
@@ -334,7 +334,8 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
       Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]
   -- f is uniformly bounded by the Gamma integrand
   · intro n
-    refine' (ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ fun x hx => _)
+    rw [ae_restrict_iff' measurableSet_Ioi]
+    filter_upwards with x hx
     dsimp only [f]
     rcases lt_or_le (n : ℝ) x with (hxn | hxn)
     · rw [indicator_of_not_mem (not_mem_Ioc_of_gt hxn), norm_zero,

Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

@@ -295,12 +295,12 @@ theorem tendsto_logGammaSeq_of_le_one (hf_conv : ConvexOn ℝ (Ioi 0) f)
   -- Porting note: `show` no longer reorders goals
   pick_goal 4
   show ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1
-  · refine' Eventually.mp (eventually_ne_atTop 0) (eventually_of_forall fun n hn => _)
-    exact le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv (@hf_feq) hx hn)
+  · filter_upwards [eventually_ne_atTop 0] with n hn using
+      le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)
   -- Porting note: `show` no longer reorders goals
   pick_goal 3
   show ∀ᶠ n : ℕ in atTop, f x - f 1 - x * (log (n + 1) - log n) ≤ logGammaSeq x n
-  · refine' eventually_of_forall fun n => _
+  · filter_upwards with n
     rw [sub_le_iff_le_add', sub_le_iff_le_add']
     convert le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1
     ring

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

@@ -280,7 +280,7 @@ theorem continuousAt_gaussian_integral (b : ℂ) (hb : 0 < re b) :
     (Complex.continuous_exp.comp (continuous_id'.neg.mul continuous_const)).continuousAt
   have f_le_bd : ∀ᶠ c : ℂ in 𝓝 b, ∀ᵐ x : ℝ, ‖f c x‖ ≤ exp (-d * x ^ 2) := by
     refine' eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') _
-    refine' fun c hc => ae_of_all _ fun x => _
+    intro c hc; filter_upwards with x
     rw [norm_cexp_neg_mul_sq]
     gcongr
     exact le_of_lt hc

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -175,8 +175,7 @@ theorem ENNReal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :
   obtain ⟨c, _, hc⟩ :=
     (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
   have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
-  refine' eventually_of_mem hc' _
-  intro a ha
+  filter_upwards [hc'] with a ha
   by_cases ha' : a = ⊤
   · simp [ha', hy]
   lift a to ℝ≥0 using ha'

Mathlib/Combinatorics/Hindman.lean

@@ -145,7 +145,7 @@ theorem exists_idempotent_ultrafilter_le_FP {M} [Semigroup M] (a : Stream' M) :
   · exact Ultrafilter.continuous_mul_left
   · apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
     · intro n U hU
-      apply Eventually.mono hU
+      filter_upwards [hU]
       rw [add_comm, ← Stream'.drop_drop, ← Stream'.tail_eq_drop]
       exact FP.tail _
     · intro n
@@ -158,11 +158,9 @@ theorem exists_idempotent_ultrafilter_le_FP {M} [Semigroup M] (a : Stream' M) :
     rw [Set.mem_iInter] at *
     intro n
     rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
-    apply Eventually.mono (hU n)
-    intro m hm
+    filter_upwards [hU n] with m hm
     obtain ⟨n', hn⟩ := FP.mul hm
-    apply Eventually.mono (hV (n' + n))
-    intro m' hm'
+    filter_upwards [hV (n' + n)] with m' hm'
     apply hn
     simpa only [Stream'.drop_drop] using hm'
 set_option linter.uppercaseLean3 false in

Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

@@ -298,7 +298,7 @@ lemma growsPolynomially_id : GrowsPolynomially (fun x => x) := by
   intro b hb
   refine ⟨b, hb.1, ?_⟩
   refine ⟨1, by norm_num, ?_⟩
-  refine eventually_of_forall fun x u hu => ?_
+  filter_upwards with x u hu
   simp only [one_mul, ge_iff_le, gt_iff_lt, not_le, Set.mem_Icc]
   exact ⟨hu.1, hu.2⟩
 

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

@@ -98,9 +98,9 @@ theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SigmaFinite ν] 
   have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂ν) := by
     rw [tendsto_pi_nhds]; intro x
     by_cases hfx : Integrable (f x) ν
-    · have : ∀ n, Integrable (s' n x) ν := by
-        intro n; apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
-        apply eventually_of_forall; intro y
+    · have (n) : Integrable (s' n x) ν := by
+        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
+        filter_upwards with y
         simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
       simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
         mem_setOf_eq]
@@ -162,7 +162,7 @@ theorem integrable_measure_prod_mk_left {s : Set (α × β)} (hs : MeasurableSet
   -- Porting note: was `simp_rw`
   rw [prod_apply hs]
   apply lintegral_congr_ae
-  refine' (ae_measure_lt_top hs h2s).mp _; apply eventually_of_forall; intro x hx
+  filter_upwards [ae_measure_lt_top hs h2s] with x hx
   rw [lt_top_iff_ne_top] at hx; simp [ofReal_toReal, hx]
 #align measure_theory.measure.integrable_measure_prod_mk_left MeasureTheory.Measure.integrable_measure_prod_mk_left
 
@@ -237,7 +237,7 @@ theorem hasFiniteIntegral_prod_iff ⦃f : α × β → E⦄ (h1f : StronglyMeasu
   simp only [HasFiniteIntegral]
   -- porting note (#10745): was `simp`
   rw [lintegral_prod_of_measurable _ h1f.ennnorm]
-  have : ∀ x, ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := fun x => eventually_of_forall fun y => norm_nonneg _
+  have (x) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
   simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
       (h1f.norm.comp_measurable measurable_prod_mk_left).aestronglyMeasurable,
     ennnorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_coe_nnnorm]
@@ -246,7 +246,7 @@ theorem hasFiniteIntegral_prod_iff ⦃f : α × β → E⦄ (h1f : StronglyMeasu
     rw [← and_congr_right_iff, and_iff_right_of_imp h1]
   rw [this]
   · intro h2f; rw [lintegral_congr_ae]
-    refine' h2f.mp _; apply eventually_of_forall; intro x hx; dsimp only
+    filter_upwards [h2f] with x hx
     rw [ofReal_toReal]; rw [← lt_top_iff_ne_top]; exact hx
   · intro h2f; refine' ae_lt_top _ h2f.ne; exact h1f.ennnorm.lintegral_prod_right'
 #align measure_theory.has_finite_integral_prod_iff MeasureTheory.hasFiniteIntegral_prod_iff
@@ -469,10 +469,8 @@ theorem integral_prod (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
   · exact isClosed_eq continuous_integral continuous_integral_integral
   · rintro f g hfg - hf; convert hf using 1
     · exact integral_congr_ae hfg.symm
-    · refine' integral_congr_ae _
-      refine' (ae_ae_of_ae_prod hfg).mp _
-      apply eventually_of_forall; intro x hfgx
-      exact integral_congr_ae (ae_eq_symm hfgx)
+    · apply integral_congr_ae
+      filter_upwards [ae_ae_of_ae_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
 #align measure_theory.integral_prod MeasureTheory.integral_prod
 
 /-- Symmetric version of **Fubini's Theorem**: For integrable functions on `α × β`,

Mathlib/MeasureTheory/Covering/Differentiation.lean

@@ -841,9 +841,7 @@ theorem ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable {f : α → E} (hf :
       v.eventually_filterAt_measurableSet x] with a ha h'a
     congr 1
     apply set_lintegral_congr_fun h'a
-    apply eventually_of_forall fun y => ?_
-    intro hy
-    simp only [ha hy, indicator_of_mem]
+    filter_upwards with y hy using (by simp only [ha hy, indicator_of_mem])
   apply ENNReal.tendsto_nhds_zero.2 fun ε εpos => ?_
   obtain ⟨c, ct, xc⟩ : ∃ c ∈ t, (‖f x - c‖₊ : ℝ≥0∞) < ε / 2 := by
     simp_rw [← edist_eq_coe_nnnorm_sub]

Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

@@ -196,7 +196,7 @@ theorem rnDeriv_restrict (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
   refine (rnDeriv_withDensity_left ?_ ?_ ?_).trans (ae_of_all _ (fun x ↦ ?_))
   · exact measurable_one.aemeasurable.indicator hs
   · exact measurable_one.aemeasurable.indicator hs
-  · refine ae_of_all _ (fun x ↦ ?_)
+  · filter_upwards with x
     simp only [Set.indicator_apply, Pi.one_apply, ne_eq]
     split_ifs <;> simp [ENNReal.zero_ne_top]
   · simp [Set.indicator_apply]

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -406,7 +406,7 @@ theorem lpMeasSubgroupToLpTrim_add (hm : m ≤ m0) (f g : lpMeasSubgroup F m p 
         (lpMeasSubgroupToLpTrim_ae_eq hm g).symm)
   refine' (Lp.coeFn_add _ _).trans _
   simp_rw [lpMeasSubgroup_coe]
-  exact eventually_of_forall fun x => by rfl
+  filter_upwards with x using rfl
 #align measure_theory.Lp_meas_subgroup_to_Lp_trim_add MeasureTheory.lpMeasSubgroupToLpTrim_add
 
 theorem lpMeasSubgroupToLpTrim_neg (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -163,8 +163,7 @@ theorem condexpIndL1Fin_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSe
   push_cast
   rw [((toSpanSingleton ℝ x).compLpL 2 μ).map_add]
   refine' (Lp.coeFn_add _ _).trans _
-  refine' eventually_of_forall fun y => _
-  rfl
+  filter_upwards with y using rfl
 #align measure_theory.condexp_ind_L1_fin_disjoint_union MeasureTheory.condexpIndL1Fin_disjoint_union
 
 end CondexpIndL1Fin

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -329,8 +329,7 @@ theorem condexpL2_indicator_eq_toSpanSingleton_comp (hm : m ≤ m0) (hs : Measur
     (condexpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)
   rw [← EventuallyEq] at h_comp
   refine' EventuallyEq.trans _ h_comp.symm
-  refine' eventually_of_forall fun y => _
-  rfl
+  filter_upwards with y using rfl
 #align measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp MeasureTheory.condexpL2_indicator_eq_toSpanSingleton_comp
 
 variable {𝕜}