case empty
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120715
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type w
f : ι → Set α
⊢ (⨅ (i : ι) (_ : i ∈ ∅), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ ∅), f i)

case insert
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120715
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (⨅ (i : ι) (_ : i ∈ s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ s), f i)
⊢ (⨅ (i_1 : ι) (_ : i_1 ∈ insert i s), 𝓟 (f i_1)) = 𝓟 (⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120715
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
s : Finset ι
f : ι → Set α
⊢ (⨅ (i : ι) (_ : i ∈ s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ s), f i)
induction' s using Finset.induction_on with i s _ hs
no goals
case empty
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120715
ι✝ : Sort x
f✝ g : Filter α
s t : Set α
ι : Type w
f : ι → Set α
⊢ (⨅ (i : ι) (_ : i ∈ ∅), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ ∅), f i)
simp
no goals
case insert
α : Type u
β : Type v
γ : Type w
δ : Type ?u.120715
ι✝ : Sort x
f✝ g : Filter α
s✝ t : Set α
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (⨅ (i : ι) (_ : i ∈ s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (_ : i ∈ s), f i)
⊢ (⨅ (i_1 : ι) (_ : i_1 ∈ insert i s), 𝓟 (f i_1)) = 𝓟 (⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1)
rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]