α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.76872
ι✝ : Sort x
f✝ g : Filter α✝
s✝ t : Set α✝
ι : Type u_1
inst✝ : Finite ι
α : Type u_2
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i) → s ∈ ⨅ (i : ι), f i
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.76872
ι✝ : Sort x
f✝ g : Filter α✝
s✝ t : Set α✝
ι : Type u_1
inst✝ : Finite ι
α : Type u_2
f : ι → Filter α
s : Set α
⊢ (s ∈ ⨅ (i : ι), f i) ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
refine' ⟨exists_iInter_of_mem_iInf, _⟩
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.76872
ι✝ : Sort x
f✝ g : Filter α✝
s t✝ : Set α✝
ι : Type u_1
inst✝ : Finite ι
α : Type u_2
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ (⋂ (i : ι), t i) ∈ ⨅ (i : ι), f i
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.76872
ι✝ : Sort x
f✝ g : Filter α✝
s✝ t : Set α✝
ι : Type u_1
inst✝ : Finite ι
α : Type u_2
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i) → s ∈ ⨅ (i : ι), f i
rintro ⟨t, ht, rfl⟩
no goals
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.76872
ι✝ : Sort x
f✝ g : Filter α✝
s t✝ : Set α✝
ι : Type u_1
inst✝ : Finite ι
α : Type u_2
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ (⋂ (i : ι), t i) ∈ ⨅ (i : ι), f i
exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)