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 _`.

Author: urkud

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 }