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

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

Tactic:
simp only [mem_iInf, SetCoe.forall', biInter_eq_iInter]

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

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

Tactic:
exact dif_neg hi

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    I_1.Finite ∧
      ∃ V_1, (∀ (i : ι), V_1 i ∈ s i) ∧ (∀ i ∉ I_1, V_1 i = univ) ∧ ⋂ i, V i = ⋂ x, V_1 ↑x ∧ ⋂ i, V i = ⋂ i, V_1 i

Tactic:
refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i

case intro.intro.intro.intro.refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

case intro.intro.intro.intro.refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Proof state:
case intro.intro.intro.intro.refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Tactic:
simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
  iInter_univ, inter_univ, eq_self_iff_true, true_and]

Result:
no goals

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

Tactic:
rintro ⟨I, If, V, hV, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    I_1.Finite ∧
      ∃ V_1, (∀ (i : ι), V_1 i ∈ s i) ∧ (∀ i ∉ I_1, V_1 i = univ) ∧ ⋂ i, V i = ⋂ x, V_1 ↑x ∧ ⋂ i, V i = ⋂ i, V_1 i

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V ⟨i, hi⟩ else univ) ∈ s i

Tactic:
split_ifs

Result:
case pos
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∈ I
⊢ V ⟨i, h✝⟩ ∈ s i

case neg
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∉ I
⊢ univ ∈ s i

Proof state:
case pos
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∈ I
⊢ V ⟨i, h✝⟩ ∈ s i

case neg
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∉ I
⊢ univ ∈ s i

Tactic:
exacts [hV ⟨i,_⟩, univ_mem]

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i

Tactic:
dsimp only

Result:
case intro.intro.intro.intro.refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V ⟨i, hi⟩ else univ) ∈ s i

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

Tactic:
refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩

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