α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : 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) ↔
    ∃ I,
      Set.Finite I ∧
        ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (U = ⋂ (x : ↑I), V ↑x) ∧ U = ⋂ (i : ι), V i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : 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 : ι), V i ∈ s i) ∧
            (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (U = ⋂ (i : ι) (_ : i ∈ I), V i) ∧ U = ⋂ (i : ι), V i
simp only [mem_iInf, SetCoe.forall', biInter_eq_iInter]
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : 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) →
    ∃ I,
      Set.Finite I ∧
        ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (U = ⋂ (x : ↑I), V ↑x) ∧ U = ⋂ (i : ι), V i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : 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) ↔
    ∃ I,
      Set.Finite I ∧
        ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (U = ⋂ (x : ↑I), V ↑x) ∧ U = ⋂ (i : ι), V i
refine' ⟨_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ V_1,
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ (i : ι), ¬i ∈ I_1 → V_1 i = univ) ∧
            ((⋂ (i : ↑I), V i) = ⋂ (x : ↑I_1), V_1 ↑x) ∧ (⋂ (i : ↑I), V i) = ⋂ (i : ι), V_1 i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : 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) →
    ∃ I,
      Set.Finite I ∧
        ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ (U = ⋂ (x : ↑I), V ↑x) ∧ U = ⋂ (i : ι), V i
rintro ⟨I, If, V, hV, rfl⟩
case intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i ∈ s i

case intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : ¬i ∈ I
⊢ (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i = univ

case intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ((⋂ (i : ↑I), V i) = ⋂ (x : ↑I), (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) ↑x) ∧
    (⋂ (i : ↑I), V i) = ⋂ (i : ι), (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    Set.Finite I_1 ∧
      ∃ V_1,
        (∀ (i : ι), V_1 i ∈ s i) ∧
          (∀ (i : ι), ¬i ∈ I_1 → V_1 i = univ) ∧
            ((⋂ (i : ↑I), V i) = ⋂ (x : ↑I_1), V_1 ↑x) ∧ (⋂ (i : ↑I), V i) = ⋂ (i : ι), V_1 i
refine' ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => _, fun i hi => _, _⟩
case intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V { val := i, property := hi } else univ) ∈ s i
case intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i ∈ s i
dsimp only
case intro.intro.intro.intro.refine'_1.inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∈ I
⊢ V { val := i, property := h✝ } ∈ s i

case intro.intro.intro.intro.refine'_1.inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : ¬i ∈ I
⊢ univ ∈ s i
case intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V { val := i, property := hi } else univ) ∈ s i
split_ifs
no goals
case intro.intro.intro.intro.refine'_1.inl
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∈ I
⊢ V { val := i, property := h✝ } ∈ s i

case intro.intro.intro.intro.refine'_1.inr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : ¬i ∈ I
⊢ univ ∈ s i
exacts [hV _, univ_mem]
no goals
case intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : ¬i ∈ I
⊢ (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i = univ
exact dif_neg hi
no goals
case intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
γ : Type w
δ : Type ?u.71658
ι✝ : Sort x
f g : Filter α
s✝ t : Set α
ι : Type u_1
s : ι → Filter α
I : Set ι
If : Set.Finite I
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ((⋂ (i : ↑I), V i) = ⋂ (x : ↑I), (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) ↑x) ∧
    (⋂ (i : ↑I), V i) = ⋂ (i : ι), (fun i => if hi : i ∈ I then V { val := i, property := hi } else univ) i
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_iff]