ι✝ : Sort ?u.3007
α : Type u_2
β : Type ?u.3013
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.3007
α : Type u_2
β : Type ?u.3013
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 [biUnion_eq_iUnion]
ι✝ : Sort ?u.3007
α : Type u_2
β : Type ?u.3013
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.3007
α : Type u_2
β : Type ?u.3013
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.3007
α : Type u_2
β : Type ?u.3013
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_iUnion fun i => h i i.2