chore(order/filter/basic): implicit arg in eventually_of_forall (#3277

)

Make `l : filter α` argument of `eventually_of_forall` implicit
because everywhere in `mathlib` it was used as `eventually_of_forall _`.

src/analysis/calculus/deriv.lean

@@ -1174,7 +1174,7 @@ theorem has_strict_deriv_at_inv (hx : x ≠ 0) : has_strict_deriv_at has_inv.inv
 begin
   suffices : is_o (λ p : 𝕜 × 𝕜, (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹))
     (λ (p : 𝕜 × 𝕜), (p.1 - p.2) * 1) (𝓝 (x, x)),
-  { refine this.congr' _ (eventually_of_forall _ $ λ _, mul_one _),
+  { refine this.congr' _ (eventually_of_forall $ λ _, mul_one _),
     refine eventually.mono (mem_nhds_sets (is_open_prod is_open_ne is_open_ne) ⟨hx, hx⟩) _,
     rintro ⟨y, z⟩ ⟨hy, hz⟩,
     simp only [mem_set_of_eq] at hy hz, -- hy : y ≠ 0, hz : z ≠ 0

src/analysis/calculus/fderiv.lean

@@ -589,7 +589,7 @@ theorem filter.eventually_eq.has_strict_fderiv_at_iff
   (h : f₀ =ᶠ[𝓝 x] f₁) (h' : ∀ y, f₀' y = f₁' y) :
   has_strict_fderiv_at f₀ f₀' x ↔ has_strict_fderiv_at f₁ f₁' x :=
 begin
-  refine is_o_congr ((h.prod_mk_nhds h).mono _) (eventually_of_forall _ $ λ _, rfl),
+  refine is_o_congr ((h.prod_mk_nhds h).mono _) (eventually_of_forall $ λ _, rfl),
   rintros p ⟨hp₁, hp₂⟩,
   simp only [*]
 end
@@ -601,7 +601,7 @@ theorem has_strict_fderiv_at.congr_of_eventually_eq (h : has_strict_fderiv_at f
 theorem filter.eventually_eq.has_fderiv_at_filter_iff
   (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : ∀ x, f₀' x = f₁' x) :
   has_fderiv_at_filter f₀ f₀' x L ↔ has_fderiv_at_filter f₁ f₁' x L :=
-is_o_congr (h₀.mono $ λ y hy, by simp only [hy, h₁, hx]) (eventually_of_forall _ $ λ _, rfl)
+is_o_congr (h₀.mono $ λ y hy, by simp only [hy, h₁, hx]) (eventually_of_forall $ λ _, rfl)
 
 lemma has_fderiv_at_filter.congr_of_eventually_eq (h : has_fderiv_at_filter f f' x L)
   (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) : has_fderiv_at_filter f₁ f' x L :=
@@ -2225,11 +2225,11 @@ begin
     simp },
   refine this.trans_is_o _, clear this,
   refine ((hf.comp_tendsto hg).symm.congr' (hfg.mono _)
-    (eventually_of_forall _ $ λ _, rfl)).trans_is_O _,
+    (eventually_of_forall $ λ _, rfl)).trans_is_O _,
   { rintros p ⟨hp1, hp2⟩,
     simp [hp1, hp2] },
   { refine (hf.is_O_sub_rev.comp_tendsto hg).congr'
-      (eventually_of_forall _ $ λ _, rfl) (hfg.mono _),
+      (eventually_of_forall $ λ _, rfl) (hfg.mono _),
     rintros p ⟨hp1, hp2⟩,
     simp only [(∘), hp1, hp2] }
 end
@@ -2249,11 +2249,11 @@ begin
     simp },
   refine this.trans_is_o _, clear this,
   refine ((hf.comp_tendsto hg).symm.congr' (hfg.mono _)
-    (eventually_of_forall _ $ λ _, rfl)).trans_is_O _,
+    (eventually_of_forall $ λ _, rfl)).trans_is_O _,
   { rintros p hp,
     simp [hp, hfg.self_of_nhds] },
   { refine (hf.is_O_sub_rev.comp_tendsto hg).congr'
-      (eventually_of_forall _ $ λ _, rfl) (hfg.mono _),
+      (eventually_of_forall $ λ _, rfl) (hfg.mono _),
     rintros p hp,
     simp only [(∘), hp, hfg.self_of_nhds] }
 end

src/analysis/normed_space/bounded_linear_maps.lean

@@ -219,7 +219,7 @@ variable {f : E × F → G}
 protected lemma is_bounded_bilinear_map.is_O (h : is_bounded_bilinear_map 𝕜 f) :
   asymptotics.is_O f (λ p : E × F, ∥p.1∥ * ∥p.2∥) ⊤ :=
 let ⟨C, Cpos, hC⟩ := h.bound in asymptotics.is_O.of_bound _ $
-filter.eventually_of_forall ⊤ $ λ ⟨x, y⟩, by simpa [mul_assoc] using hC x y
+filter.eventually_of_forall $ λ ⟨x, y⟩, by simpa [mul_assoc] using hC x y
 
 lemma is_bounded_bilinear_map.is_O_comp {α : Type*} (H : is_bounded_bilinear_map 𝕜 f)
   {g : α → E} {h : α → F} {l : filter α} :

src/analysis/normed_space/multilinear.lean

@@ -512,7 +512,7 @@ begin
         apply add_le_add_right,
         simpa [dist_eq_norm] using b_bound n 0 0 (zero_le _) (zero_le _)
       end },
-    exact le_of_tendsto at_top_ne_bot (hF v).norm (eventually_of_forall _ A) },
+    exact le_of_tendsto at_top_ne_bot (hF v).norm (eventually_of_forall A) },
   -- Thus `F` is continuous, and we propose that as the limit point of our original Cauchy sequence.
   let Fcont := Fmult.mk_continuous _ Fnorm,
   use Fcont,

src/analysis/normed_space/operator_norm.lean

@@ -470,7 +470,7 @@ begin
         apply add_le_add_right,
         simpa [dist_eq_norm] using b_bound n 0 0 (zero_le _) (zero_le _)
       end },
-    exact le_of_tendsto at_top_ne_bot (hG v).norm (eventually_of_forall _ A) },
+    exact le_of_tendsto at_top_ne_bot (hG v).norm (eventually_of_forall A) },
   -- Thus `G` is continuous, and we propose that as the limit point of our original Cauchy sequence.
   let Gcont := Glin.mk_continuous _ Gnorm,
   use Gcont,

src/measure_theory/measure_space.lean

@@ -729,7 +729,7 @@ lemma measure_zero_iff_ae_nmem {s : set α} : μ s = 0 ↔ ∀ₘ a ∂ μ, a 
 by simp only [ae_iff, not_not, set_of_mem_eq]
 
 lemma ae_of_all {p : α → Prop} (μ : measure α) : (∀a, p a) → ∀ₘ a ∂ μ, p a :=
-eventually_of_forall _
+eventually_of_forall
 
 instance : countable_Inter_filter μ.ae :=
 ⟨begin

src/order/filter/at_top_bot.lean

@@ -116,7 +116,7 @@ assume h₁, (tendsto_at_top _ _).2 $ λ b, mp_sets ((tendsto_at_top _ _).1 h₁
 
 lemma tendsto_at_top_mono [preorder β] {l : filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
   tendsto f l at_top → tendsto g l at_top :=
-tendsto_at_top_mono' l $ eventually_of_forall _ h
+tendsto_at_top_mono' l $ eventually_of_forall h
 
 /-!
 ### Sequences

src/order/filter/basic.lean

@@ -840,7 +840,7 @@ inter_mem_sets
 @[simp]
 lemma eventually_true (f : filter α) : ∀ᶠ x in f, true := univ_mem_sets
 
-lemma eventually_of_forall {p : α → Prop} (f : filter α) (hp : ∀ x, p x) :
+lemma eventually_of_forall {p : α → Prop} {f : filter α} (hp : ∀ x, p x) :
   ∀ᶠ x in f, p x :=
 univ_mem_sets' hp
 
@@ -852,13 +852,13 @@ empty_in_sets_eq_bot
   (∀ᶠ x in f, p) ↔ p :=
 classical.by_cases (λ h : p, by simp [h]) (λ h, by simp [h, hf])
 
-lemma eventually.exists_mem {p : α → Prop} {f : filter α} (hp : ∀ᶠ x in f, p x) :
-  ∃ v ∈ f, ∀ y ∈ v, p y :=
- ⟨{x | p x}, hp, λ y hy, hy⟩
-
 lemma eventually_iff_exists_mem {p : α → Prop} {f : filter α} :
   (∀ᶠ x in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y :=
-⟨λ hp, hp.exists_mem, λ ⟨v, vf, hv⟩, eventually_of_mem vf hv⟩
+exists_sets_subset_iff.symm
+
+lemma eventually.exists_mem {p : α → Prop} {f : filter α} (hp : ∀ᶠ x in f, p x) :
+  ∃ v ∈ f, ∀ y ∈ v, p y :=
+eventually_iff_exists_mem.1 hp
 
 lemma eventually.mp {p q : α → Prop} {f : filter α} (hp : ∀ᶠ x in f, p x)
   (hq : ∀ᶠ x in f, p x → q x) :
@@ -868,7 +868,7 @@ mp_sets hp hq
 lemma eventually.mono {p q : α → Prop} {f : filter α} (hp : ∀ᶠ x in f, p x)
   (hq : ∀ x, p x → q x) :
   ∀ᶠ x in f, q x :=
-hp.mp (f.eventually_of_forall hq)
+hp.mp (eventually_of_forall hq)
 
 @[simp] lemma eventually_and {p q : α → Prop} {f : filter α} :
   (∀ᶠ x in f, p x ∧ q x) ↔ (∀ᶠ x in f, p x) ∧ (∀ᶠ x in f, q x) :=
@@ -939,7 +939,7 @@ end
 
 lemma frequently_of_forall {f : filter α} (hf : f ≠ ⊥) {p : α → Prop} (h : ∀ x, p x) :
   ∃ᶠ x in f, p x :=
-eventually.frequently hf (f.eventually_of_forall h)
+eventually.frequently hf (eventually_of_forall h)
 
 lemma frequently.mp {p q : α → Prop} {f : filter α} (h : ∃ᶠ x in f, p x)
   (hpq : ∀ᶠ x in f, p x → q x) :
@@ -949,7 +949,7 @@ mt (λ hq, hq.mp $ hpq.mono $ λ x, mt) h
 lemma frequently.mono {p q : α → Prop} {f : filter α} (h : ∃ᶠ x in f, p x)
   (hpq : ∀ x, p x → q x) :
   ∃ᶠ x in f, q x :=
-h.mp (f.eventually_of_forall hpq)
+h.mp (eventually_of_forall hpq)
 
 lemma frequently.and_eventually {p q : α → Prop} {f : filter α}
   (hp : ∃ᶠ x in f, p x) (hq : ∀ᶠ x in f, q x) :
@@ -963,7 +963,7 @@ end
 lemma frequently.exists {p : α → Prop} {f : filter α} (hp : ∃ᶠ x in f, p x) : ∃ x, p x :=
 begin
   by_contradiction H,
-  replace H : ∀ᶠ x in f, ¬ p x, from f.eventually_of_forall (not_exists.1 H),
+  replace H : ∀ᶠ x in f, ¬ p x, from eventually_of_forall (not_exists.1 H),
   exact hp H
 end
 
@@ -1104,7 +1104,7 @@ eventually_iff_exists_mem
 
 @[refl] lemma eventually_eq.refl (l : filter α) (f : α → β) :
   f =ᶠ[l] f :=
-eventually_of_forall l $ λ x, rfl
+eventually_of_forall $ λ x, rfl
 
 @[symm] lemma eventually_eq.symm {f g : α → β} {l : filter α} (H : f =ᶠ[l] g) :
   g =ᶠ[l] f :=

src/order/filter/filter_product.lean

@@ -49,7 +49,7 @@ protected def field [field β] (U : is_ultrafilter φ) : field β* :=
 /-- If `φ` is an ultrafilter then the ultraproduct is a linear order.
 This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
 protected def linear_order [linear_order β] (U : is_ultrafilter φ) : linear_order β* :=
-{ le_total := λ f g, induction_on₂ f g $ λ f g, U.eventually_or.1 $ eventually_of_forall _ $
+{ le_total := λ f g, induction_on₂ f g $ λ f g, U.eventually_or.1 $ eventually_of_forall $
     λ x, le_total _ _,
   .. germ.partial_order }
 

src/order/filter/germ.lean

@@ -204,7 +204,7 @@ iff.rfl
 
 lemma lift_pred_const {p : β → Prop} {x : β} (hx : p x) :
   lift_pred p (↑x : germ l β) :=
-eventually_of_forall _ $ λ y, hx
+eventually_of_forall $ λ y, hx
 
 @[simp] lemma lift_pred_const_iff (hl : l ≠ ⊥) {p : β → Prop} {x : β} :
   lift_pred p (↑x : germ l β) ↔ p x :=
@@ -221,7 +221,7 @@ iff.rfl
 
 lemma lift_rel_const {r : β → γ → Prop} {x : β} {y : γ} (h : r x y) :
   lift_rel r (↑x : germ l β) ↑y :=
-eventually_of_forall _ $ λ _, h
+eventually_of_forall $ λ _, h
 
 @[simp] lemma lift_rel_const_iff (hl : l ≠ ⊥) {r : β → γ → Prop} {x : β} {y : γ} :
   lift_rel r (↑x : germ l β) ↑y ↔ r x y :=
@@ -446,7 +446,7 @@ instance [has_bot β] : has_bot (germ l β) := ⟨↑(⊥:β)⟩
 instance [order_bot β] : order_bot (germ l β) :=
 { bot := ⊥,
   le := (≤),
-  bot_le := λ f, induction_on f $ λ f, eventually_of_forall _ $ λ x, bot_le,
+  bot_le := λ f, induction_on f $ λ f, eventually_of_forall $ λ x, bot_le,
   .. germ.partial_order }
 
 instance [has_top β] : has_top (germ l β) := ⟨↑(⊤:β)⟩
@@ -456,7 +456,7 @@ instance [has_top β] : has_top (germ l β) := ⟨↑(⊤:β)⟩
 instance [order_top β] : order_top (germ l β) :=
 { top := ⊤,
   le := (≤),
-  le_top := λ f, induction_on f $ λ f, eventually_of_forall _ $ λ x, le_top,
+  le_top := λ f, induction_on f $ λ f, eventually_of_forall $ λ x, le_top,
   .. germ.partial_order }
 
 instance [has_sup β] : has_sup (germ l β) := ⟨map₂ (⊔)⟩
@@ -470,19 +470,19 @@ instance [has_inf β] : has_inf (germ l β) := ⟨map₂ (⊓)⟩
 instance [semilattice_sup β] : semilattice_sup (germ l β) :=
 { sup := (⊔),
   le_sup_left := λ f g, induction_on₂ f g $ λ f g,
-    eventually_of_forall _ $ λ x, le_sup_left,
+    eventually_of_forall $ λ x, le_sup_left,
   le_sup_right := λ f g, induction_on₂ f g $ λ f g,
-    eventually_of_forall _ $ λ x, le_sup_right,
+    eventually_of_forall $ λ x, le_sup_right,
   sup_le := λ f₁ f₂ g, induction_on₃ f₁ f₂ g $ λ f₁ f₂ g h₁ h₂,
     h₂.mp $ h₁.mono $ λ x, sup_le,
   .. germ.partial_order }
 
 instance [semilattice_inf β] : semilattice_inf (germ l β) :=
 { inf := (⊓),
   inf_le_left := λ f g, induction_on₂ f g $ λ f g,
-    eventually_of_forall _ $ λ x, inf_le_left,
+    eventually_of_forall $ λ x, inf_le_left,
   inf_le_right := λ f g, induction_on₂ f g $ λ f g,
-    eventually_of_forall _ $ λ x, inf_le_right,
+    eventually_of_forall $ λ x, inf_le_right,
   le_inf := λ f₁ f₂ g, induction_on₃ f₁ f₂ g $ λ f₁ f₂ g h₁ h₂,
     h₂.mp $ h₁.mono $ λ x, le_inf,
   .. germ.partial_order }

src/order/liminf_limsup.lean

@@ -63,7 +63,7 @@ iff.intro
 /-- A bounded function `u` is in particular eventually bounded. -/
 lemma is_bounded_under_of {f : filter β} {u : β → α} :
   (∃b, ∀x, r (u x) b) → f.is_bounded_under r u
-| ⟨b, hb⟩ := ⟨b, show ∀ᶠ x in f, r (u x) b, from eventually_of_forall _ hb⟩
+| ⟨b, hb⟩ := ⟨b, show ∀ᶠ x in f, r (u x) b, from eventually_of_forall hb⟩
 
 lemma is_bounded_bot : is_bounded r ⊥ ↔ nonempty α :=
 by simp [is_bounded, exists_true_iff_nonempty]
@@ -147,11 +147,11 @@ lemma is_cobounded_ge_of_top [order_top α] {f : filter α} : f.is_cobounded (
 ⟨⊤, assume a h, le_top⟩
 
 lemma is_bounded_le_of_top [order_top α] {f : filter α} : f.is_bounded (≤) :=
-⟨⊤, eventually_of_forall _ $ λ _, le_top⟩
+⟨⊤, eventually_of_forall $ λ _, le_top⟩
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma is_bounded_ge_of_bot [order_bot α] {f : filter α} : f.is_bounded (≥) :=
-⟨⊥, eventually_of_forall _ $ λ _, bot_le⟩
+⟨⊥, eventually_of_forall $ λ _, bot_le⟩
 
 lemma is_bounded_under_sup [semilattice_sup α] {f : filter β} {u v : β → α} :
   f.is_bounded_under (≤) u → f.is_bounded_under (≤) v → f.is_bounded_under (≤) (λa, u a ⊔ v a)

src/topology/algebra/ordered.lean

@@ -145,23 +145,23 @@ show (a₁, a₂) ∈ {p:α×α | p.1 ≤ p.2},
 lemma le_of_tendsto_of_tendsto' {f g : β → α} {b : filter β} {a₁ a₂ : α} (hb : b ≠ ⊥)
   (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) :
   a₁ ≤ a₂ :=
-le_of_tendsto_of_tendsto hb hf hg (eventually_of_forall _ h)
+le_of_tendsto_of_tendsto hb hf hg (eventually_of_forall h)
 
 lemma le_of_tendsto {f : β → α} {a b : α} {x : filter β}
   (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b :=
 le_of_tendsto_of_tendsto nt lim tendsto_const_nhds h
 
 lemma le_of_tendsto' {f : β → α} {a b : α} {x : filter β}
   (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : ∀ c, f c ≤ b) : a ≤ b :=
-le_of_tendsto nt lim (eventually_of_forall _ h)
+le_of_tendsto nt lim (eventually_of_forall h)
 
 lemma ge_of_tendsto {f : β → α} {a b : α} {x : filter β}
   (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a :=
 le_of_tendsto_of_tendsto nt tendsto_const_nhds lim h
 
 lemma ge_of_tendsto' {f : β → α} {a b : α} {x : filter β}
   (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : ∀ c, b ≤ f c) : b ≤ a :=
-ge_of_tendsto nt lim (eventually_of_forall _ h)
+ge_of_tendsto nt lim (eventually_of_forall h)
 
 @[simp]
 lemma closure_le_eq [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
@@ -442,7 +442,7 @@ lemma tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : filter
   (hg : tendsto g b (𝓝 a)) (hh : tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) :
   tendsto f b (𝓝 a) :=
 tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh
-  (eventually_of_forall _ hgf) (eventually_of_forall _ hfh)
+  (eventually_of_forall hgf) (eventually_of_forall hfh)
 
 lemma nhds_order_unbounded {a : α} (hu : ∃u, a < u) (hl : ∃l, l < a) :
   𝓝 a = (⨅l (h₂ : l < a) u (h₂ : a < u), 𝓟 (Ioo l u)) :=
@@ -1691,7 +1691,7 @@ variables [semilattice_sup α] [topological_space α] [order_topology α]
 
 lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
 match forall_le_or_exists_lt_sup a with
-| or.inl h := ⟨a, eventually_of_forall _ h⟩
+| or.inl h := ⟨a, eventually_of_forall h⟩
 | or.inr ⟨b, hb⟩ := ⟨b, ge_mem_nhds hb⟩
 end
 
@@ -1716,7 +1716,7 @@ variables [semilattice_inf α] [topological_space α] [order_topology α]
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) :=
 match forall_le_or_exists_lt_inf a with
-| or.inl h := ⟨a, eventually_of_forall _ h⟩
+| or.inl h := ⟨a, eventually_of_forall h⟩
 | or.inr ⟨b, hb⟩ := ⟨b, le_mem_nhds hb⟩
 end
 
@@ -1930,7 +1930,7 @@ begin
       cases exists_lt_of_lt_csupr h with N hN,
       apply eventually.mono (mem_at_top N),
       exact λ i hi, lt_of_lt_of_le hN (h_mono hi) },
-    { exact λ a h, eventually_of_forall _ (λ n, lt_of_le_of_lt (le_csupr hbdd n) h) } },
+    { exact λ a h, eventually_of_forall (λ n, lt_of_le_of_lt (le_csupr hbdd n) h) } },
   { exact tendsto_of_not_nonempty hi }
 end