case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (U ∈ ⨅ (i : ι), s i) → ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i

case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i) → U ∈ ⨅ (i : ι), s i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (U ∈ ⨅ (i : ι), s i) ↔ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
constructor
case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U) → ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (U ∈ ⨅ (i : ι), s i) → ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
rw [iInf_eq_generate, mem_generate_iff]
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite t
tinter : ⋂₀ t ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (∃ t x, Set.Finite t ∧ ⋂₀ t ⊆ U) → ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
rintro ⟨t, tsub, tfin, tinter⟩
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂₀ ⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite t
tinter : ⋂₀ t ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂₀ ⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
rw [sInter_iUnion] at tinter
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
set V := fun i => U ∪ ⋂₀ σ i with hV
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑{i | i ∈ I}), V i ∈ s ↑i
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
have V_in : ∀ i, V i ∈ s i := by
  rintro i
  have : ⋂₀ σ i ∈ s i := by
    rw [sInter_mem (σfin _)]
    apply σsub
  exact mem_of_superset this (subset_union_right _ _)
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑{i | i ∈ I}), V i ∈ s ↑i
⊢ U = ⋂ (i : ↑I), V i
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑{i | i ∈ I}), V i ∈ s ↑i
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
refine' ⟨I, Ifin, V, V_in, _⟩
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑{i | i ∈ I}), V i ∈ s ↑i
⊢ U = ⋂ (i : ↑I), V i
rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
⊢ V i ∈ s ↑i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∀ (i : ↑{i | i ∈ I}), V i ∈ s ↑i
rintro i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
this : ⋂₀ σ i ∈ s ↑i
⊢ V i ∈ s ↑i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
⊢ V i ∈ s ↑i
have : ⋂₀ σ i ∈ s i := by
  rw [sInter_mem (σfin _)]
  apply σsub
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
this : ⋂₀ σ i ∈ s ↑i
⊢ V i ∈ s ↑i
exact mem_of_superset this (subset_union_right _ _)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
⊢ ∀ (U : Set α), U ∈ σ i → U ∈ s ↑i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
⊢ ⋂₀ σ i ∈ s ↑i
rw [sInter_mem (σfin _)]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
I : Set ι
Ifin : Set.Finite I
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), Set.Finite (σ i)
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : (⋃ (i : ↑{i | i ∈ I}), σ i) ⊆ ⋃ (i : ι), (s i).sets
tfin : Set.Finite (⋃ (i : ↑{i | i ∈ I}), σ i)
tinter : (⋂ (i : ↑{i | i ∈ I}), ⋂₀ σ i) ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑{i | i ∈ I}
⊢ ∀ (U : Set α), U ∈ σ i → U ∈ s ↑i
apply σsub
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
Ifin : Set.Finite I
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ (⋂ (i : ↑I), V i) ∈ ⨅ (i : ι), s i
case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
U : Set α
⊢ (∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i) → U ∈ ⨅ (i : ι), s i
rintro ⟨I, Ifin, V, V_in, rfl⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.69710
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
Ifin : Set.Finite I
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ (⋂ (i : ↑I), V i) ∈ ⨅ (i : ι), s i
exact mem_iInf_of_iInter Ifin V_in Subset.rfl