feat(lint): improved ge_or_gt linter (#3810)

The linter will now correctly accepts occurrences of `f (≥)` and `∃ x ≥ t, b`
The linter will still raise a false positive on `∃ x y ≥ t, b` (with 2+ bound variables in a single binder that involves `>/≥`)
In contrast to the previous version of the linter, this one *does* check hypotheses.
This should reduce the `@[nolint ge_or_gt]` attributes from ~160 to ~10.

src/algebra/order.lean

@@ -63,10 +63,12 @@ end lt
 end has_lt
 
 namespace ge
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma le [has_le α] {x y : α} (h : x ≥ y) : y ≤ x := h
 end ge
 
 namespace gt
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma lt [has_lt α] {x y : α} (h : x > y) : y < x := h
 end gt
 

src/algebra/ordered_group.lean

@@ -477,7 +477,6 @@ iff.intro
 lemma zero_lt_iff_ne_zero : 0 < a ↔ a ≠ 0 :=
 iff.intro ne_of_gt $ assume hne, lt_of_le_of_ne (zero_le _) hne.symm
 
-@[nolint ge_or_gt]
 lemma exists_pos_add_of_lt (h : a < b) : ∃ c > 0, a + c = b :=
 begin
   obtain ⟨c, hc⟩ := le_iff_exists_add.1 (le_of_lt h),

src/analysis/convex/cone.lean

@@ -208,11 +208,9 @@ end
 
 variables {s : set E} (hs : convex s) {x : E}
 
-@[nolint ge_or_gt]
 lemma mem_to_cone : x ∈ hs.to_cone s ↔ ∃ (c > 0) (y ∈ s), (c : ℝ) • y = x :=
 by simp only [to_cone, convex_cone.mem_mk, mem_Union, mem_smul_set, eq_comm, exists_prop]
 
-@[nolint ge_or_gt]
 lemma mem_to_cone' : x ∈ hs.to_cone s ↔ ∃ c > 0, (c : ℝ) • x ∈ s :=
 begin
   refine hs.mem_to_cone.trans ⟨_, _⟩,
@@ -331,7 +329,6 @@ begin
         mul_inv_cancel (ne_of_gt hr), one_mul] at this } }
 end
 
-@[nolint ge_or_gt]
 theorem exists_top (p : linear_pmap ℝ E ℝ)
   (hp_nonneg : ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x)
   (hp_dense : ∀ y, ∃ x : p.domain, (x : E) + y ∈ s) :

src/analysis/hofer.lean

@@ -24,7 +24,6 @@ open filter finset
 
 local notation `d` := dist
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma hofer {X: Type*} [metric_space X] [complete_space X]
   (x : X) (ε : ℝ) (ε_pos : 0 < ε)
   {ϕ : X → ℝ} (cont : continuous ϕ) (nonneg : ∀ y, 0 ≤ ϕ y) :

src/analysis/normed_space/banach.lean

@@ -32,7 +32,6 @@ Rescaling everything, it follows that any `y ∈ F` is arbitrarily well approach
 images of elements of norm at most `C * ∥y∥`.
 For further use, we will only need such an element whose image
 is within distance `∥y∥/2` of `y`, to apply an iterative process. -/
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma exists_approx_preimage_norm_le (surj : surjective f) :
   ∃C ≥ 0, ∀y, ∃x, dist (f x) y ≤ 1/2 * ∥y∥ ∧ ∥x∥ ≤ C * ∥y∥ :=
 begin
@@ -110,7 +109,6 @@ variable [complete_space E]
 
 /-- The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then
 any point has a preimage with controlled norm. -/
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem exists_preimage_norm_le (surj : surjective f) :
   ∃C > 0, ∀y, ∃x, f x = y ∧ ∥x∥ ≤ C * ∥y∥ :=
 begin

src/analysis/normed_space/basic.lean

@@ -195,7 +195,6 @@ calc
   ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
   ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H }
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
 metric.tendsto_nhds.trans $ by simp only [dist_zero_right]
@@ -1030,7 +1029,6 @@ lemma has_sum_of_bounded_monoid_hom_of_summable
   has_sum (λ (b:ι), φ (f b)) (φ (∑'b, f b)) :=
 has_sum_of_bounded_monoid_hom_of_has_sum hf.has_sum C hφ
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → α} :
   cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
 begin
@@ -1044,7 +1042,6 @@ begin
     exact ht u hu }
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma summable_iff_vanishing_norm [complete_space α] {f : ι → α} :
   summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
 by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]

src/data/complex/exponential.lean

@@ -237,7 +237,6 @@ finset.induction_on s (by simp [abv_zero abv])
   (λ a s has ih, by rw [sum_insert has, sum_insert has];
     exact le_trans (abv_add abv _ _) (add_le_add_left ih _))
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma cauchy_product {a b : ℕ → β}
   (ha : is_cau_seq abs (λ m, ∑ n in range m, abv (a n)))
   (hb : is_cau_seq abv (λ m, ∑ n in range m, b n)) (ε : α) (ε0 : 0 < ε) :

src/data/list/basic.lean

@@ -1262,7 +1262,7 @@ lemma remove_nth_insert_nth (n:ℕ) (l : list α) : (l.insert_nth n a).remove_nt
 by rw [remove_nth_eq_nth_tail, insert_nth, modify_nth_tail_modify_nth_tail_same];
 from modify_nth_tail_id _ _
 
-lemma insert_nth_remove_nth_of_ge : ∀n m as, n < length as → m ≥ n →
+lemma insert_nth_remove_nth_of_ge : ∀n m as, n < length as → n ≤ m →
   insert_nth m a (as.remove_nth n) = (as.insert_nth (m + 1) a).remove_nth n
 | 0     0     []      has _   := (lt_irrefl _ has).elim
 | 0     0     (a::as) has hmn := by simp [remove_nth, insert_nth]

src/data/real/cau_seq.lean

@@ -100,7 +100,6 @@ instance abs_is_absolute_value {α} [discrete_linear_ordered_field α] :
 
 open is_absolute_value
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem exists_forall_ge_and {α} [linear_order α] {P Q : α → Prop} :
   (∃ i, ∀ j ≥ i, P j) → (∃ i, ∀ j ≥ i, Q j) →
   ∃ i, ∀ j ≥ i, P j ∧ Q j
@@ -111,15 +110,13 @@ section
 variables {α : Type*} [discrete_linear_ordered_field α]
   {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem rat_add_continuous_lemma
   {ε : α} (ε0 : 0 < ε) : ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β},
   abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε :=
 ⟨ε / 2, half_pos ε0, λ a₁ a₂ b₁ b₂ h₁ h₂,
   by simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
     using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)⟩
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem rat_mul_continuous_lemma
   {ε K₁ K₂ : α} (ε0 : 0 < ε) :
   ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ →
@@ -138,7 +135,6 @@ begin
     using lt_of_le_of_lt (abv_add abv _ _) this
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem rat_inv_continuous_lemma
   {β : Type*} [field β] (abv : β → α) [is_absolute_value abv]
   {ε K : α} (ε0 : 0 < ε) (K0 : 0 < K) :
@@ -178,7 +174,6 @@ begin
   rw abv_sub abv, exact hi _ ik
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem cauchy₃ (hf : is_cau_seq abv f) {ε : α} (ε0 : 0 < ε) :
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε :=
 let ⟨i, H⟩ := hf.cauchy₂ ε0 in ⟨i, λ j ij k jk, H _ _ (le_trans ij jk) ij⟩
@@ -207,7 +202,6 @@ subtype.eq (funext h)
 
 theorem is_cau (f : cau_seq β abv) : is_cau_seq abv f := f.2
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem cauchy (f : cau_seq β abv) :
   ∀ {ε}, 0 < ε → ∃ i, ∀ j ≥ i, abv (f j - f i) < ε := f.2
 
@@ -222,7 +216,6 @@ variable [is_absolute_value abv]
 theorem cauchy₂ (f : cau_seq β abv) {ε} : 0 < ε →
   ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε := f.2.cauchy₂
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem cauchy₃ (f : cau_seq β abv) {ε} : 0 < ε →
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε := f.2.cauchy₃
 
@@ -243,7 +236,6 @@ begin
     rw [add_sub, add_comm] at this, simpa }
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem bounded' (f : cau_seq β abv) (x : α) : ∃ r > x, ∀ i, abv (f i) < r :=
 let ⟨r, h⟩ := f.bounded in
 ⟨max r (x+1), lt_of_lt_of_le (lt_add_one _) (le_max_right _ _),
@@ -366,7 +358,6 @@ instance equiv : setoid (cau_seq β abv) :=
  λ f g h, by simpa using neg_lim_zero h,
  λ f g h fg gh, by simpa [sub_eq_add_neg, add_assoc] using add_lim_zero fg gh⟩⟩
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem equiv_def₃ {f g : cau_seq β abv} (h : f ≈ g) {ε : α} (ε0 : 0 < ε) :
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
 (exists_forall_ge_and (h _ $ half_pos ε0) (f.cauchy₃ $ half_pos ε0)).imp $
@@ -378,7 +369,6 @@ theorem lim_zero_congr {f g : cau_seq β abv} (h : f ≈ g) : lim_zero f ↔ lim
 ⟨λ l, by simpa using add_lim_zero (setoid.symm h) l,
  λ l, by simpa using add_lim_zero h l⟩
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem abv_pos_of_not_lim_zero {f : cau_seq β abv} (hf : ¬ lim_zero f) :
   ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (f j) :=
 begin
@@ -471,7 +461,6 @@ end integral_domain
 section field
 variables {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem inv_aux {f : cau_seq β abv} (hf : ¬ lim_zero f) :
   ∀ ε > 0, ∃ i, ∀ j ≥ i, abv ((f j)⁻¹ - (f i)⁻¹) < ε | ε ε0 :=
 let ⟨K, K0, HK⟩ := abv_pos_of_not_lim_zero hf,

src/dynamics/periodic_pts.lean

@@ -164,23 +164,19 @@ lemma directed_pts_of_period_pnat (f : α → α) : directed (⊆) (λ n : ℕ+,
 λ m n, ⟨m * n, λ x hx, hx.mul_const n, λ x hx, hx.const_mul m⟩
 
 /-- The set of periodic points of a map `f : α → α`. -/
-@[nolint ge_or_gt]
 def periodic_pts (f : α → α) : set α := {x : α | ∃ n > 0, is_periodic_pt f n x}
 
 lemma mk_mem_periodic_pts (hn : 0 < n) (hx : is_periodic_pt f n x) :
   x ∈ periodic_pts f :=
 ⟨n, hn, hx⟩
 
-@[nolint ge_or_gt]
 lemma mem_periodic_pts : x ∈ periodic_pts f ↔ ∃ n > 0, is_periodic_pt f n x := iff.rfl
 
 variable (f)
 
-@[nolint ge_or_gt]
 lemma bUnion_pts_of_period : (⋃ n > 0, pts_of_period f n) = periodic_pts f :=
 set.ext $ λ x, by simp [mem_periodic_pts]
 
-@[nolint ge_or_gt]
 lemma Union_pnat_pts_of_period : (⋃ n : ℕ+, pts_of_period f n) = periodic_pts f :=
 supr_subtype.trans $ bUnion_pts_of_period f
 

src/group_theory/order_of_element.lean

@@ -85,7 +85,6 @@ have a ^ (i - j) = 1,
   by simp [sub_eq_add_neg, gpow_add, gpow_neg, a_eq],
 ⟨i - j, sub_ne_zero.mpr ne, this⟩
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma exists_pow_eq_one (a : α) : ∃i > 0, a ^ i = 1 :=
 let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
 begin

src/order/basic.lean

@@ -419,7 +419,6 @@ lemma eq_of_le_of_forall_ge_of_dense [linear_order α] [densely_ordered α] {a
   (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃<a₁, a₃ ≤ a₂) : a₁ = a₂ :=
 le_antisymm (le_of_forall_ge_of_dense h₂) h₁
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma dense_or_discrete [linear_order α] (a₁ a₂ : α) :
   (∃a, a₁ < a ∧ a < a₂) ∨ ((∀a>a₁, a₂ ≤ a) ∧ (∀a<a₂, a ≤ a₁)) :=
 classical.or_iff_not_imp_left.2 $ assume h,

src/order/complete_lattice.lean

@@ -256,7 +256,6 @@ iff.intro
     let ⟨a, ha, h⟩ := h _ h' in
     lt_irrefl a $ lt_of_le_of_lt (le_Sup ha) h)
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma Inf_eq_bot : Inf s = ⊥ ↔ (∀b>⊥, ∃a∈s, a < b) :=
 @Sup_eq_top (order_dual α) _ _
 
@@ -829,7 +828,6 @@ variables [complete_linear_order α]
 lemma supr_eq_top (f : ι → α) : supr f = ⊤ ↔ (∀b<⊤, ∃i, b < f i) :=
 by simp only [← Sup_range, Sup_eq_top, set.exists_range_iff]
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma infi_eq_bot (f : ι → α) : infi f = ⊥ ↔ (∀b>⊥, ∃i, f i < b) :=
 by simp only [← Inf_range, Inf_eq_bot, set.exists_range_iff]
 

src/order/filter/at_top_bot.lean

@@ -60,12 +60,12 @@ lemma at_top_basis' [semilattice_sup α] (a : α) :
 lemma at_top_ne_bot [nonempty α] [semilattice_sup α] : ne_bot (at_top : filter α) :=
 at_top_basis.forall_nonempty_iff_ne_bot.1 $ λ a _, nonempty_Ici
 
-@[simp, nolint ge_or_gt]
+@[simp]
 lemma mem_at_top_sets [nonempty α] [semilattice_sup α] {s : set α} :
   s ∈ (at_top : filter α) ↔ ∃a:α, ∀b≥a, b ∈ s :=
 at_top_basis.mem_iff.trans $ exists_congr $ λ _, exists_const _
 
-@[simp, nolint ge_or_gt]
+@[simp]
 lemma eventually_at_top [semilattice_sup α] [nonempty α] {p : α → Prop} :
   (∀ᶠ x in at_top, p x) ↔ (∃ a, ∀ b ≥ a, p b) :=
 mem_at_top_sets
@@ -89,17 +89,14 @@ lemma tendsto_at_top_pure [order_top α] (f : α → β) :
   tendsto f at_top (pure $ f ⊤) :=
 (order_top.at_top_eq α).symm ▸ tendsto_pure_pure _ _
 
-@[nolint ge_or_gt]
 lemma eventually.exists_forall_of_at_top [semilattice_sup α] [nonempty α] {p : α → Prop}
   (h : ∀ᶠ x in at_top, p x) : ∃ a, ∀ b ≥ a, p b :=
 eventually_at_top.mp h
 
-@[nolint ge_or_gt]
 lemma frequently_at_top [semilattice_sup α] [nonempty α] {p : α → Prop} :
   (∃ᶠ x in at_top, p x) ↔ (∀ a, ∃ b ≥ a, p b) :=
 by simp only [filter.frequently, eventually_at_top, not_exists, not_forall, not_not]
 
-@[nolint ge_or_gt]
 lemma frequently_at_top' [semilattice_sup α] [nonempty α] [no_top_order α] {p : α → Prop} :
   (∃ᶠ x in at_top, p x) ↔ (∀ a, ∃ b > a, p b) :=
 begin
@@ -112,7 +109,6 @@ begin
     exact ⟨b, le_of_lt hb, hb'⟩ },
 end
 
-@[nolint ge_or_gt]
 lemma frequently.forall_exists_of_at_top [semilattice_sup α] [nonempty α] {p : α → Prop}
   (h : ∃ᶠ x in at_top, p x) : ∀ a, ∃ b ≥ a, p b :=
 frequently_at_top.mp h
@@ -142,7 +138,6 @@ tendsto_at_top_mono' l $ eventually_of_forall h
 ### Sequences
 -/
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma inf_map_at_top_ne_bot_iff [semilattice_sup α] [nonempty α] {F : filter β} {u : α → β} :
   ne_bot (F ⊓ (map u at_top)) ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U :=
 by simp_rw [inf_ne_bot_iff_frequently_left, frequently_map, frequently_at_top]; refl
@@ -166,7 +161,6 @@ lemma extraction_of_eventually_at_top {P : ℕ → Prop} (h : ∀ᶠ n in at_top
   ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
 extraction_of_frequently_at_top h.frequently
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma exists_le_of_tendsto_at_top [semilattice_sup α] [preorder β] {u : α → β}
   (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b ≤ u a' :=
 begin
@@ -178,7 +172,6 @@ begin
   exact ⟨a', ha, hb⟩
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma exists_lt_of_tendsto_at_top [semilattice_sup α] [preorder β] [no_top_order β]
   {u : α → β} (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b < u a' :=
 begin
@@ -192,7 +185,6 @@ end
 If `u` is a sequence which is unbounded above,
 then after any point, it reaches a value strictly greater than all previous values.
 -/
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma high_scores [linear_order β] [no_top_order β] {u : ℕ → β}
   (hu : tendsto u at_top at_top) : ∀ N, ∃ n ≥ N, ∀ k < n, u k < u n :=
 begin
@@ -339,7 +331,6 @@ end ordered_group
 
 open_locale filter
 
-@[nolint ge_or_gt]
 lemma tendsto_at_top' [nonempty α] [semilattice_sup α] (f : α → β) (l : filter β) :
   tendsto f at_top l ↔ (∀s ∈ l, ∃a, ∀b≥a, f b ∈ s) :=
 by simp only [tendsto_def, mem_at_top_sets]; refl
@@ -348,7 +339,6 @@ lemma tendsto_at_bot' [nonempty α] [semilattice_inf α] (f : α → β) (l : fi
   tendsto f at_bot l ↔ (∀s ∈ l, ∃a, ∀b≤a, f b ∈ s) :=
 @tendsto_at_top' (order_dual α) _ _ _ _ _
 
-@[nolint ge_or_gt]
 theorem tendsto_at_top_principal [nonempty β] [semilattice_sup β] {f : β → α} {s : set α} :
   tendsto f at_top (𝓟 s) ↔ ∃N, ∀n≥N, f n ∈ s :=
 by rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_at_top_sets]; refl

src/order/filter/bases.lean

@@ -360,7 +360,6 @@ lemma has_basis.eq_infi (h : l.has_basis (λ _, true) s) :
   l = ⨅ i, 𝓟 (s i) :=
 by simpa only [infi_true] using h.eq_binfi
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma has_basis_infi_principal {s : ι → set α} (h : directed (≥) s) [nonempty ι] :
   (⨅ i, 𝓟 (s i)).has_basis (λ _, true) s :=
 ⟨begin
@@ -379,7 +378,6 @@ begin
     exists_finite_iff_finset, finset.bInter_coe]
 end
 
-@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma has_basis_binfi_principal {s : β → set α} {S : set β} (h : directed_on (s ⁻¹'o (≥)) S)
   (ne : S.nonempty) :
   (⨅ i ∈ S, 𝓟 (s i)).has_basis (λ i, i ∈ S) s :=

src/order/filter/basic.lean

@@ -590,7 +590,6 @@ lemma mem_infi {f : ι → filter α} (h : directed (≥) f) [nonempty ι] (s) :
   s ∈ infi f ↔ ∃ i, s ∈ f i :=
 by simp only [infi_sets_eq h, mem_Union]
 
-@[nolint ge_or_gt] -- Intentional use of `≥`
 lemma binfi_sets_eq {f : β → filter α} {s : set β}
   (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) :
   (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets) :=
@@ -599,7 +598,6 @@ calc (⨅ i ∈ s, f i).sets  = (⨅ t : {t // t ∈ s}, (f t.val)).sets : by rw
   ... = (⨆ t : {t // t ∈ s}, (f t.val).sets) : infi_sets_eq h.directed_coe
   ... = (⨆ t ∈ s, (f t).sets) : by rw [supr_subtype]; refl
 
-@[nolint ge_or_gt] -- Intentional use of `≥`
 lemma mem_binfi {f : β → filter α} {s : set β}
   (h : directed_on (f ⁻¹'o (≥)) s) (ne : s.nonempty) {t : set α} :
   t ∈ (⨅ i∈s, f i) ↔ ∃ i ∈ s, t ∈ f i :=