filter_upwards for a finite family

Stream: Is there code for X?

[Kevin Buzzard]

I have this

import Mathlib

example (X : Type*) (F : Filter X) (A B : Type*) [Fintype A] [Fintype B]
    (s : A → B → X → Prop) (hs : ∀ a b, ∀ᶠ x in F, s a b x)
    (Q : X → Prop) (hQ : ∀ x, (∀ a b, s a b x) → Q x) :
    ∀ᶠ x in F, Q x := by
  sorry

and I'd like to use filter_upwards or perhaps a lemma to reduce the goal to hQ. I had hoped filter_upwards [hs] would work but it doesn't seem to. I know I can just bash everything out using the axioms of a filter but is there a slick way to reduce my goal to hQ using hs?

(Mathematically, s : A \times B \to Set X is a finite family of sets, hs says they're all in F, so their intersection is in F, and hQ says that the intersection is contained in the set corresponding to Q so that's in F too)

[Yongxi Lin (Aaron)]

I think this Filter.eventually_all_finset will be useful, but it only works for Finsets and not for Fintypes

[Yongxi Lin (Aaron)]

Suppose we have sth like Filter.eventually_all_finset that works for Fintypes, then you can switch the quantifier twice to turn the type of hs into ∀ᶠ x in F, ∀ a b, s a b x, and then you can probably filter_upwards [hs].

[Kevin Buzzard]

Oh thanks, this is perfect:

  simp_rw [← Filter.eventually_all] at hs
  filter_upwards [hs]

works in my application.