chore(order/filter, *): enhancing filter_upwards tactic (#11624)

src/analysis/ODE/picard_lindelof.lean

@@ -227,8 +227,7 @@ begin
       (f.continuous_v_comp.measurable_at_filter _ _) f.continuous_v_comp.continuous_within_at,
   rw v_comp_apply_coe at this,
   refine this.congr_of_eventually_eq_of_mem _ t.coe_prop,
-  filter_upwards [self_mem_nhds_within],
-  intros t' ht',
+  filter_upwards [self_mem_nhds_within] with _ ht',
   rw v.proj_of_mem ht'
 end
 

src/analysis/analytic/basic.lean

@@ -489,8 +489,8 @@ begin
     from hf.uniform_geometric_approx' h,
   refine is_O_iff.2 ⟨C * (a / r') ^ n, _⟩,
   replace r'0 : 0 < (r' : ℝ), by exact_mod_cast r'0,
-  filter_upwards [metric.ball_mem_nhds (0 : E) r'0], intros y hy,
-  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div] using hp y hy n
+  filter_upwards [metric.ball_mem_nhds (0 : E) r'0] with y hy,
+  simpa [mul_pow, mul_div_assoc, mul_assoc, div_mul_eq_mul_div] using hp y hy n,
 end
 
 -- hack to speed up simp when dealing with complicated types

src/analysis/analytic/inverse.lean

@@ -478,7 +478,7 @@ begin
     have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1/2,
       by { apply (tendsto_order.1 this).2, simp [zero_lt_one] },
     have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a,
-      by { filter_upwards [self_mem_nhds_within], exact λ a ha, ha },
+      by { filter_upwards [self_mem_nhds_within] with _ ha using ha },
     rcases (C.and ((A.and B).filter_mono inf_le_left)).exists with ⟨a, ha⟩,
     exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩ },
   -- check by induction that the partial sums are suitably bounded, using the choice of `a` and the

src/analysis/asymptotics/asymptotics.lean

@@ -187,9 +187,8 @@ begin
   unfold is_O_with,
   subst c₂,
   apply filter.eventually_congr,
-  filter_upwards [hf, hg],
-  assume x e₁ e₂,
-  rw [e₁, e₂]
+  filter_upwards [hf, hg] with _ e₁ e₂,
+  rw [e₁, e₂],
 end
 
 theorem is_O_with.congr' {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
@@ -300,8 +299,7 @@ theorem is_O_with.trans (hfg : is_O_with c f g l) (hgk : is_O_with c' g k l) (hc
   is_O_with (c * c') f k l :=
 begin
   unfold is_O_with at *,
-  filter_upwards [hfg, hgk],
-  assume x hx hx',
+  filter_upwards [hfg, hgk] with x hx hx',
   calc ∥f x∥ ≤ c * ∥g x∥ : hx
   ... ≤ c * (c' * ∥k x∥) : mul_le_mul_of_nonneg_left hx' hc
   ... = c * c' * ∥k x∥ : (mul_assoc _ _ _).symm
@@ -535,7 +533,7 @@ end
 
 lemma is_O_with.prod_left_same (hf : is_O_with c f' k' l) (hg : is_O_with c g' k' l) :
   is_O_with c (λ x, (f' x, g' x)) k' l :=
-by rw is_O_with_iff at *; filter_upwards [hf, hg] λ x, max_le
+by rw is_O_with_iff at *; filter_upwards [hf, hg] with x using max_le
 
 lemma is_O_with.prod_left (hf : is_O_with c f' k' l) (hg : is_O_with c' g' k' l) :
   is_O_with (max c c') (λ x, (f' x, g' x)) k' l :=
@@ -594,7 +592,7 @@ variables {c₁ c₂ : ℝ} {f₁ f₂ : α → E'}
 
 theorem is_O_with.add (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_O_with c₂ f₂ g l) :
   is_O_with (c₁ + c₂) (λ x, f₁ x + f₂ x) g l :=
-by rw is_O_with at *; filter_upwards [h₁, h₂] λ x hx₁ hx₂,
+by rw is_O_with at *; filter_upwards [h₁, h₂] with x hx₁ hx₂ using
 calc ∥f₁ x + f₂ x∥ ≤ c₁ * ∥g x∥ + c₂ * ∥g x∥ : norm_add_le_of_le hx₁ hx₂
                ... = (c₁ + c₂) * ∥g x∥       : (add_mul _ _ _).symm
 
@@ -970,8 +968,7 @@ theorem is_O_with.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c
   is_O_with (c₁ * c₂) (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
 begin
   unfold is_O_with at *,
-  filter_upwards [h₁, h₂],
-  intros x hx₁ hx₂,
+  filter_upwards [h₁, h₂] with _ hx₁ hx₂,
   apply le_trans (norm_mul_le _ _),
   convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1,
   rw normed_field.norm_mul,

src/analysis/box_integral/divergence_theorem.lean

@@ -177,8 +177,7 @@ begin
       { exact Ioc_mem_nhds_within_Ioi ⟨le_rfl, one_half_pos⟩ },
       { rcases ((nhds_within_has_basis nhds_basis_closed_ball _).tendsto_iff
           nhds_basis_closed_ball).1 (Hs x hx.2) _ (half_pos $ half_pos ε0) with ⟨δ₁, δ₁0, hδ₁⟩,
-        filter_upwards [Ioc_mem_nhds_within_Ioi ⟨le_rfl, δ₁0⟩],
-        rintro δ hδ y₁ hy₁ y₂ hy₂,
+        filter_upwards [Ioc_mem_nhds_within_Ioi ⟨le_rfl, δ₁0⟩] with δ hδ y₁ hy₁ y₂ hy₂,
         have : closed_ball x δ ∩ I.Icc ⊆ closed_ball x δ₁ ∩ I.Icc,
           from inter_subset_inter_left _ (closed_ball_subset_closed_ball hδ.2),
         rw ← dist_eq_norm,

src/analysis/calculus/fderiv.lean

@@ -299,7 +299,7 @@ begin
   refine le_of_forall_pos_le_add (λ ε ε0, op_norm_le_of_nhds_zero _ _),
   exact add_nonneg hC₀ ε0.le,
   rw [← map_add_left_nhds_zero x₀, eventually_map] at hlip,
-  filter_upwards [is_o_iff.1 (has_fderiv_at_iff_is_o_nhds_zero.1 hf) ε0, hlip], intros y hy hyC,
+  filter_upwards [is_o_iff.1 (has_fderiv_at_iff_is_o_nhds_zero.1 hf) ε0, hlip] with y hy hyC,
   rw add_sub_cancel' at hyC,
   calc ∥f' y∥ ≤ ∥f (x₀ + y) - f x₀∥ + ∥f (x₀ + y) - f x₀ - f' y∥ : norm_le_insert _ _
           ... ≤ C * ∥y∥ + ε * ∥y∥                                : add_le_add hyC hy
@@ -312,8 +312,7 @@ lemma has_fderiv_at.le_of_lip {f : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf
   {s : set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0} (hlip : lipschitz_on_with C f s) : ∥f'∥ ≤ C :=
 begin
   refine hf.le_of_lip' C.coe_nonneg _,
-  filter_upwards [hs],
-  exact λ x hx, hlip.norm_sub_le hx (mem_of_mem_nhds hs)
+  filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs),
 end
 
 theorem has_fderiv_at_filter.mono (h : has_fderiv_at_filter f f' x L₂) (hst : L₁ ≤ L₂) :

src/analysis/calculus/fderiv_symmetric.lean

@@ -87,10 +87,9 @@ begin
   have E2 : ∀ᶠ h in 𝓝[>] (0:ℝ), (h : ℝ) < 1 :=
     mem_nhds_within_Ioi_iff_exists_Ioo_subset.2
       ⟨(1 : ℝ), by simp only [mem_Ioi, zero_lt_one], λ x hx, hx.2⟩,
-  filter_upwards [E1, E2, self_mem_nhds_within],
+  filter_upwards [E1, E2, self_mem_nhds_within] with h hδ h_lt_1 hpos,
   -- we consider `h` small enough that all points under consideration belong to this ball,
   -- and also with `0 < h < 1`.
-  assume h hδ h_lt_1 hpos,
   replace hpos : 0 < h := hpos,
   have xt_mem : ∀ t ∈ Icc (0 : ℝ) 1, x + h • v + (t * h) • w ∈ interior s,
   { assume t ht,
@@ -264,9 +263,8 @@ begin
       rw [← one_smul ℝ (f'' w v - f'' v w), smul_smul, smul_smul],
       congr' 1,
       field_simp [has_lt.lt.ne' hpos] },
-    { filter_upwards [self_mem_nhds_within],
-      assume h hpos,
-      field_simp [has_lt.lt.ne' hpos, has_scalar.smul] } },
+    { filter_upwards [self_mem_nhds_within] with _ hpos,
+      field_simp [has_lt.lt.ne' hpos, has_scalar.smul], }, },
   simpa only [sub_eq_zero] using (is_o_const_const_iff (@one_ne_zero ℝ _ _)).1 B,
 end
 

src/analysis/calculus/parametric_integral.lean

@@ -117,8 +117,7 @@ begin
   rw [has_fderiv_at_iff_tendsto, tendsto_congr' this, ← tendsto_zero_iff_norm_tendsto_zero,
       ← show ∫ (a : α), ∥x₀ - x₀∥⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ = 0, by simp],
   apply tendsto_integral_filter_of_dominated_convergence,
-  { filter_upwards [h_ball],
-    intros x x_in,
+  { filter_upwards [h_ball] with _ x_in,
     apply ae_measurable.const_smul,
     exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuous_linear_map _) },
   { apply mem_of_superset h_ball,

src/analysis/calculus/specific_functions.lean

@@ -100,8 +100,7 @@ lemma f_aux_deriv_pos (n : ℕ) (x : ℝ) (hx : 0 < x) :
   has_deriv_at (f_aux n) ((P_aux (n+1)).eval x * exp (-x⁻¹) / x^(2 * (n + 1))) x :=
 begin
   apply (f_aux_deriv n x (ne_of_gt hx)).congr_of_eventually_eq,
-  filter_upwards [lt_mem_nhds hx],
-  assume y hy,
+  filter_upwards [lt_mem_nhds hx] with _ hy,
   simp [f_aux, hy.not_le]
 end
 
@@ -162,8 +161,7 @@ begin
   { have : f_aux (n+1) x = 0, by simp [f_aux, le_of_lt hx],
     rw this,
     apply (has_deriv_at_const x (0 : ℝ)).congr_of_eventually_eq,
-    filter_upwards [gt_mem_nhds hx],
-    assume y hy,
+    filter_upwards [gt_mem_nhds hx] with _ hy,
     simp [f_aux, hy.le] },
   { have : f_aux (n + 1) 0 = 0, by simp [f_aux, le_refl],
     rw [hx, this],

src/analysis/calculus/tangent_cone.lean

@@ -152,8 +152,7 @@ begin
   choose d' hd' using this,
   refine ⟨c, λn, (d n, d' n), _, hc, _⟩,
   show ∀ᶠ n in at_top, (x, y) + (d n, d' n) ∈ s ×ˢ t,
-  { filter_upwards [hd],
-    assume n hn,
+  { filter_upwards [hd] with n hn,
     simp [hn, (hd' n).1] },
   { apply tendsto.prod_mk_nhds hy _,
     refine squeeze_zero_norm (λn, (hd' n).2.le) _,
@@ -174,8 +173,7 @@ begin
   choose d' hd' using this,
   refine ⟨c, λn, (d' n, d n), _, hc, _⟩,
   show ∀ᶠ n in at_top, (x, y) + (d' n, d n) ∈ s ×ˢ t,
-  { filter_upwards [hd],
-    assume n hn,
+  { filter_upwards [hd] with n hn,
     simp [hn, (hd' n).1] },
   { apply tendsto.prod_mk_nhds _ hy,
     refine squeeze_zero_norm (λn, (hd' n).2.le) _,

src/analysis/complex/cauchy_integral.lean

@@ -419,8 +419,7 @@ begin
     rw [mem_insert_iff, not_or_distrib] at hzws,
     refine (((differentiable_at_id.sub_const w).inv $ sub_ne_zero.2 hzws.1).smul
       ((hd z ⟨hzR, hzws.2⟩).sub_const (f w))).congr_of_eventually_eq _,
-    filter_upwards [is_open_ne.mem_nhds hzws.1],
-    exact λ x hx, update_noteq hx _ _ },
+    filter_upwards [is_open_ne.mem_nhds hzws.1] with x hx using update_noteq hx _ _ },
   have HI := circle_integral_eq_zero_of_differentiable_on_off_countable hR.le hws hcF hdF,
   have hne : ∀ z ∈ sphere c R, z ≠ w, from λ z hz, ne_of_mem_of_not_mem hz (ne_of_lt hw.1),
   have hFeq : eq_on F (λ z, (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R),

src/analysis/convex/integral.lean

@@ -84,9 +84,8 @@ lemma convex.smul_integral_mem
   (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s :=
 begin
   have : ∀ᵐ (x : α) ∂μ, hfi.ae_measurable.mk f x ∈ s,
-  { filter_upwards [hfs, hfi.ae_measurable.ae_eq_mk],
-    assume a ha h,
-    rwa ← h },
+  { filter_upwards [hfs, hfi.ae_measurable.ae_eq_mk] with _ _ h,
+    rwa ← h, },
   convert convex.smul_integral_mem_of_measurable hs hsc hμ this
     (hfi.congr hfi.ae_measurable.ae_eq_mk) (hfi.ae_measurable.measurable_mk) using 2,
   apply integral_congr_ae,

src/analysis/fourier.lean

@@ -230,8 +230,7 @@ begin
   transitivity ∫ t : circle, conj ((fourier_Lp 2 i : circle → ℂ) t) * f t ∂ haar_circle,
   { simp [fourier_series.repr_apply_apply f i, measure_theory.L2.inner_def] },
   apply integral_congr_ae,
-  filter_upwards [coe_fn_fourier_Lp 2 i],
-  intros t ht,
+  filter_upwards [coe_fn_fourier_Lp 2 i] with _ ht,
   rw [ht, ← fourier_neg],
   simp [-fourier_neg]
 end

src/analysis/normed_space/basic.lean

@@ -317,8 +317,7 @@ begin
   have r0' : 0 < ∥r∥ := norm_pos_iff.2 r0,
   rcases exists_between r0' with ⟨ε, ε0, εr⟩,
   have : ∀ᶠ e in 𝓝 r, ∥e⁻¹ - r⁻¹∥ ≤ ∥r - e∥ / ∥r∥ / ε,
-  { filter_upwards [(is_open_lt continuous_const continuous_norm).eventually_mem εr],
-    intros e he,
+  { filter_upwards [(is_open_lt continuous_const continuous_norm).eventually_mem εr] with e he,
     have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he),
     calc ∥e⁻¹ - r⁻¹∥ = ∥r - e∥ / ∥r∥ / ∥e∥ : by field_simp [mul_comm]
     ... ≤ ∥r - e∥ / ∥r∥ / ε :

src/analysis/normed_space/exponential.lean

@@ -239,8 +239,7 @@ lemma exp_series_radius_eq_top : (exp_series 𝕂 𝔸).radius = ∞ :=
 begin
   refine (exp_series 𝕂 𝔸).radius_eq_top_of_summable_norm (λ r, _),
   refine summable_of_norm_bounded_eventually _ (real.summable_pow_div_factorial r) _,
-  filter_upwards [eventually_cofinite_ne 0],
-  intros n hn,
+  filter_upwards [eventually_cofinite_ne 0] with n hn,
   rw [norm_mul, norm_norm (exp_series 𝕂 𝔸 n), exp_series, norm_smul, norm_div, norm_one, norm_pow,
       nnreal.norm_eq, norm_eq_abs, abs_cast_nat, mul_comm, ←mul_assoc, ←mul_div_assoc, mul_one],
   have : ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕂 n 𝔸∥ ≤ 1 :=

src/analysis/normed_space/pointwise.lean

@@ -89,8 +89,7 @@ begin
   obtain ⟨R, Rpos, hR⟩ : ∃ (R : ℝ), 0 < R ∧ s ⊆ closed_ball 0 R := hs.subset_ball_lt 0 0,
   have : metric.closed_ball (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) :=
     closed_ball_mem_nhds _ (div_pos εpos Rpos),
-  filter_upwards [this],
-  assume r hr,
+  filter_upwards [this] with r hr,
   simp only [image_add_left, singleton_add],
   assume y hy,
   obtain ⟨z, zs, hz⟩ : ∃ (z : E), z ∈ s ∧ r • z = -x + y, by simpa [mem_smul_set] using hy,

src/analysis/special_functions/bernstein.lean

@@ -221,8 +221,8 @@ begin
   intros ε h,
   let δ := δ f ε h,
   have nhds_zero := tendsto_const_div_at_top_nhds_0_nat (2 * ∥f∥ * δ ^ (-2 : ℤ)),
-  filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_at_top 0],
-  intros n nh npos',
+  filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_at_top 0]
+    with n nh npos',
   have npos : 0 < (n:ℝ) := by exact_mod_cast npos',
   -- Two easy inequalities we'll need later:
   have w₁ : 0 ≤ 2 * ∥f∥ := mul_nonneg (by norm_num) (norm_nonneg f),

src/analysis/special_functions/complex/arg.lean

@@ -395,9 +395,8 @@ begin
     tendsto (λ x : ℂ, real.arcsin ((-x).im / x.abs) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π)),
   { refine H.congr' _,
     have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0, from continuous_re.tendsto z (gt_mem_nhds hre),
-    filter_upwards [self_mem_nhds_within, mem_nhds_within_of_mem_nhds this],
-    intros w him hre,
-    rw [arg, if_neg hre.not_le, if_neg him.not_le] },
+    filter_upwards [self_mem_nhds_within, mem_nhds_within_of_mem_nhds this] with _ him hre,
+    rw [arg, if_neg hre.not_le, if_neg him.not_le], },
   convert (real.continuous_at_arcsin.comp_continuous_within_at
     ((continuous_im.continuous_at.comp_continuous_within_at continuous_within_at_neg).div
       continuous_abs.continuous_within_at _)).sub tendsto_const_nhds,
@@ -411,8 +410,7 @@ lemma continuous_within_at_arg_of_re_neg_of_im_zero
 begin
   have : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] λ x, real.arcsin ((-x).im / x.abs) + π,
   { have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0, from continuous_re.tendsto z (gt_mem_nhds hre),
-    filter_upwards [self_mem_nhds_within, mem_nhds_within_of_mem_nhds this],
-    intros w him hre,
+    filter_upwards [self_mem_nhds_within, mem_nhds_within_of_mem_nhds this] with _ him hre,
     rw [arg, if_neg hre.not_le, if_pos him] },
   refine continuous_within_at.congr_of_eventually_eq _ this _,
   { refine (real.continuous_at_arcsin.comp_continuous_within_at

src/analysis/special_functions/exponential.lean

@@ -92,8 +92,7 @@ begin
     exact has_fderiv_at_exp_zero_of_radius_pos hpos },
   have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius :=
     emetric.ball_mem_nhds _ hpos,
-  filter_upwards [this],
-  intros h hh,
+  filter_upwards [this] with _ hh,
   rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, continuous_linear_map.id_apply, smul_eq_mul],
   ring
 end

src/analysis/special_functions/non_integrable.lean

@@ -139,8 +139,7 @@ lemma not_interval_integrable_of_sub_inv_is_O_punctured {f : ℝ → F} {a b c :
   ¬interval_integrable f volume a b :=
 begin
   have A : ∀ᶠ x in 𝓝[≠] c, has_deriv_at (λ x, real.log (x - c)) (x - c)⁻¹ x,
-  { filter_upwards [self_mem_nhds_within],
-    intros x hx,
+  { filter_upwards [self_mem_nhds_within] with x hx,
     simpa using ((has_deriv_at_id x).sub_const c).log (sub_ne_zero.2 hx) },
   have B : tendsto (λ x, ∥real.log (x - c)∥) (𝓝[≠] c) at_top,
   { refine tendsto_abs_at_bot_at_top.comp (real.tendsto_log_nhds_within_zero.comp _),

src/analysis/special_functions/trigonometric/basic.lean

@@ -827,7 +827,7 @@ begin
   apply tendsto_nhds_within_of_tendsto_nhds_of_eventually_within,
   { convert continuous_cos.continuous_within_at, simp },
   { filter_upwards [Ioo_mem_nhds_within_Iio (right_mem_Ioc.mpr (norm_num.lt_neg_pos
-      _ _ pi_div_two_pos pi_div_two_pos))] λ x hx, cos_pos_of_mem_Ioo hx },
+      _ _ pi_div_two_pos pi_div_two_pos))] with x hx using cos_pos_of_mem_Ioo hx },
 end
 
 lemma tendsto_tan_pi_div_two : tendsto tan (𝓝[<] (π/2)) at_top :=
@@ -845,7 +845,7 @@ begin
   apply tendsto_nhds_within_of_tendsto_nhds_of_eventually_within,
   { convert continuous_cos.continuous_within_at, simp },
   { filter_upwards [Ioo_mem_nhds_within_Ioi (left_mem_Ico.mpr (norm_num.lt_neg_pos
-      _ _ pi_div_two_pos pi_div_two_pos))] λ x hx, cos_pos_of_mem_Ioo hx },
+      _ _ pi_div_two_pos pi_div_two_pos))] with x hx using cos_pos_of_mem_Ioo hx },
 end
 
 lemma tendsto_tan_neg_pi_div_two : tendsto tan (𝓝[>] (-(π/2))) at_bot :=

src/analysis/special_functions/trigonometric/inverse_deriv.lean

@@ -82,8 +82,8 @@ begin
   refine ⟨_, λ h, (has_deriv_within_at_arcsin_Ici h).differentiable_within_at⟩,
   rintro h rfl,
   have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id,
-  { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩],
-    exact λ x, sin_arcsin' },
+  { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩]
+      with x using sin_arcsin', },
   have := h.has_deriv_within_at.sin.congr_of_eventually_eq this.symm (by simp),
   simpa using (unique_diff_on_Ici _ _ left_mem_Ici).eq_deriv _ this (has_deriv_within_at_id _ _)
 end

src/analysis/specific_limits.lean

@@ -814,11 +814,10 @@ begin
   { push_neg at hr₀,
     refine summable_of_norm_bounded_eventually 0 summable_zero _,
     rw nat.cofinite_eq_at_top,
-    filter_upwards [h],
-    intros n hn,
+    filter_upwards [h] with _ hn,
     by_contra h,
     push_neg at h,
-    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn $ mul_neg_of_neg_of_pos hr₀ h) }
+    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn $ mul_neg_of_neg_of_pos hr₀ h), },
 end
 
 lemma summable_of_ratio_test_tendsto_lt_one {α : Type*} [normed_group α] [complete_space α]
@@ -827,9 +826,8 @@ lemma summable_of_ratio_test_tendsto_lt_one {α : Type*} [normed_group α] [comp
 begin
   rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩,
   refine summable_of_ratio_norm_eventually_le hr₁ _,
-  filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf],
-  intros n h₀ h₁,
-  rwa ← div_le_iff (norm_pos_iff.mpr h₁)
+  filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf] with _ _ h₁,
+  rwa ← div_le_iff (norm_pos_iff.mpr h₁),
 end
 
 lemma not_summable_of_ratio_norm_eventually_ge {α : Type*} [semi_normed_group α]
@@ -860,14 +858,12 @@ lemma not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [semi_normed_group
   (h : tendsto (λ n, ∥f (n+1)∥/∥f n∥) at_top (𝓝 l)) : ¬ summable f :=
 begin
   have key : ∀ᶠ n in at_top, ∥f n∥ ≠ 0,
-  { filter_upwards [eventually_ge_of_tendsto_gt hl h],
-    intros n hn hc,
+  { filter_upwards [eventually_ge_of_tendsto_gt hl h] with _ hn hc,
     rw [hc, div_zero] at hn,
     linarith },
   rcases exists_between hl with ⟨r, hr₀, hr₁⟩,
   refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently _,
-  filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key],
-  intros n h₀ h₁,
+  filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key] with _ _ h₁,
   rwa ← le_div_iff (lt_of_le_of_ne (norm_nonneg _) h₁.symm)
 end
 

src/analysis/subadditive.lean

@@ -93,9 +93,7 @@ begin
       tendsto_const_nhds.add (tendsto_const_nhds.div_at_top tendsto_coe_nat_at_top_at_top),
     rw add_zero at this,
     exact (tendsto_order.1 this).2 _ wL },
-  filter_upwards [B, C],
-  assume p hp h'p,
-  exact hp.trans_lt h'p
+  filter_upwards [B, C] with _ hp h'p using hp.trans_lt h'p,
 end
 
 /-- Fekete's lemma: a subadditive sequence which is bounded below converges. -/

src/dynamics/ergodic/conservative.lean

@@ -129,7 +129,7 @@ begin
   simp only [frequently_at_top, @forall_swap (_ ∈ s), ae_all_iff],
   intro n,
   filter_upwards [measure_zero_iff_ae_nmem.1 (hf.measure_mem_forall_ge_image_not_mem_eq_zero hs n)],
-  simp
+  simp,
 end
 
 lemma inter_frequently_image_mem_ae_eq (hf : conservative f μ) (hs : measurable_set s) :