α : Type u
β : Type v
γ : Type w
δ : Type ?u.68937
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
I_fin : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : (⋂ (i : ↑I), V i) ⊆ U
this : Fintype ↑I
⊢ U ∈ ⨅ (i : ι), s i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.68937
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
I_fin : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : (⋂ (i : ↑I), V i) ⊆ U
⊢ U ∈ ⨅ (i : ι), s i
haveI := I_fin.fintype
α : Type u
β : Type v
γ : Type w
δ : Type ?u.68937
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
I_fin : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : (⋂ (i : ↑I), V i) ⊆ U
this : Fintype ↑I
i : ↑I
⊢ V i ∈ ⨅ (i : ι), s i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.68937
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
I_fin : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : (⋂ (i : ↑I), V i) ⊆ U
this : Fintype ↑I
⊢ U ∈ ⨅ (i : ι), s i
refine' mem_of_superset (iInter_mem.2 fun i => _) hU
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.68937
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
I_fin : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : (⋂ (i : ↑I), V i) ⊆ U
this : Fintype ↑I
i : ↑I
⊢ V i ∈ ⨅ (i : ι), s i
exact mem_iInf_of_mem (i : ι) (hV _)