-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
simp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) ↔
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₁ :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ (x : (↑I : Type u_2)), V (↑x : ι) ∧ U = ⋂ (i : ι), V i
simp₂ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    ∃ (I_1 : Set ι),
      I_1.Finite ∧
        ∃ (V_1 : ι → Set α),
          (∀ (i : ι), V_1 i ∈ s i) ∧
            (∀ i ∉ I_1, V_1 i = univ) ∧
              Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (x : (↑I_1 : Type u_2)), V_1 (↑x : ι)) ∧
                Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i) (⋂ (i : ι), V_1 i)
refine_1 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι),
    (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i
refine_2 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι)
    (hi : i ∉ I),
    Eq.{u + 1} (α := Set α)
      ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
refine_3 :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
        (⋂ (x : (↑I : Type u_2)),
          (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α))
            (↑x : ι)) ∧
      Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
        (⋂ (i : ι),
          (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i)
refine_2₁ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) (i : ι)
    (hi : i ∉ I),
    Eq.{u + 1} (α := Set α)
      ((fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i) univ
refine_3₁ refine_3₂ :
  ∀ (I : Set ι) (If : I.Finite) (V : (↑I : Type u_2) → Set α) (hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)),
    Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
        (⋂ (x : (↑I : Type u_2)),
          (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α))
            (↑x : ι)) ∧
      Eq.{u + 1} (α := Set α) (⋂ (i : (↑I : Type u_2)), V i)
        (⋂ (i : ι),
          (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) U ↔
    ∃ (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

Tactic:
classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]

Premises used: Filter.mem_iInf, Subtype.coe_prop, Set.inter_univ, Set.iInter_univ, Set.biInter_eq_iInter, dif_pos, Subtype.coe_eta, Filter.univ_mem, Set.iInter_dite, rfl, true_and