ι✝ : Sort ?u.5259
α : Type u_2
β : Type ?u.5265
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
ι✝ : Sort ?u.5259
α : Type u_2
β : Type ?u.5265
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ (⋂ (i : ι) (h : i ∈ S), s i h) ≤ᶠ[l] ⋂ (i : ι) (h : i ∈ S), t i h
simp only [biInter_eq_iInter]
ι✝ : Sort ?u.5259
α : Type u_2
β : Type ?u.5265
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
ι✝ : Sort ?u.5259
α : Type u_2
β : Type ?u.5265
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
haveI := hS.toEncodable
no goals
ι✝ : Sort ?u.5259
α : Type u_2
β : Type ?u.5265
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_1
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ (⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S)) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
exact EventuallyLE.countable_iInter fun i => h i i.2