-- Mathlib/Order/Filter/Finite.lean
theorem mem_iInf {ι} {s : ι → Filter α} {U : Set α} :
    (U ∈ ⨅ i, s i) ↔
      ∃ I : Set ι, I.Finite ∧ ∃ V : I → Set α, (∀ (i : I), V i ∈ s i) ∧ U = ⋂ i, V i

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
refine ⟨I, Ifin, V, V_in, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = ⋂ i, V i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
⊢ ∀ U ∈ σ i, U ∈ s ↑i

Tactic:
apply σsub

Result:
no goals

Proof state:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rw [iInf_eq_generate, mem_generate_iff]

Result:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ t ⊆ ⋃ i, (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
set V := fun i => U ∪ ⋂₀ σ i with hV

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Proof state:
case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i

Tactic:
rintro ⟨I, Ifin, V, V_in, rfl⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : ↑I → Set α
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i ∈ ⨅ i, s i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
⊢ ⋂₀ σ i ∈ s ↑i

Tactic:
rw [sInter_mem (σfin _)]

Result:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
⊢ ∀ U ∈ σ i, U ∈ s ↑i

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
have V_in : ∀ (i : 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

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i => U ∪ ⋂₀ σ i
hV : V = fun i => U ∪ ⋂₀ σ i
i : ↑I
this : ⋂₀ σ i ∈ s ↑i
⊢ V i ∈ s ↑i

Tactic:
exact mem_of_superset this subset_union_right

Result:
no goals

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
constructor

Result:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i

Proof state:
case mp.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ i, (s i).sets
tfin : t.Finite
tinter : ⋂₀ t ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂₀ ⋃ i, σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂₀ ⋃ i, σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rw [sInter_iUnion] at tinter

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i