awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ (i : ι), (s i).sets
tfin : t.Finite
tinter : ⋂₀ t ⊆ U
mp :
  ∀ (I : Set ι) (Ifin : I.Finite) (σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α))
    (σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite)
    (σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets)
    (tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets))
    (tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i))
    (tinter : ⋂₀ ⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ U),
    ∃ (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 : (↑I : Type u_2) → Set α), (∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)) ∧ U = ⋂ (i : (↑I : Type u_2)), V i

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

Premises used: Set.eq_finite_iUnion_of_finite_subset_iUnion, rfl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂₀ ⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ U
⊢ ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U

Tactic:
rw [sInter_iUnion] at tinter

Premises used: Set.sInter_iUnion
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
⊢ let V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i;
  V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i

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

Premises used: Union.union, Set.sInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
rw : ∀ U ∈ σ i, U ∈ s (↑i : ι)
⊢ ⋂₀ σ i ∈ s (↑i : ι)

Tactic:
rw [sInter_mem (σfin _)]

Premises used: Filter.sInter_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
⊢ ∀ U ∈ σ i, U ∈ s (↑i : ι)

Tactic:
apply σsub
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
⊢ ⋂₀ σ i ∈ s (↑i : ι)

Tactic:
have : ⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
this : ⋂₀ σ i ∈ s (↑i : ι)
⊢ V i ∈ s (↑i : ι)

Tactic:
mem_of_superset this subset_union_right

Premises used: Set.subset_union_right, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
i : (↑I : Type u_2)
this : ⋂₀ σ i ∈ s (↑i : ι)
⊢ V i ∈ s (↑i : ι)

Tactic:
exact mem_of_superset this subset_union_right

Premises used: Set.subset_union_right, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
⊢ ∀ (i : (↑I : Type u_2)), V i ∈ s (↑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
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
⊢ ∃ (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

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
mp : U = ⋂ (i : (↑I : Type u_2)), V i
⊢ ∃ (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

Tactic:
refine ⟨I, Ifin, V, V_in, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : (↑{i : ι | i ∈ I} : Type u_2) → Set (Set α)
σfin : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), (σ i).Finite
σsub : ∀ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i ⊆ (s (↑i : ι)).sets
tsub : Subset.{u} (α := Set (Set α)) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i) (⋃ (i : ι), (s i).sets)
tfin : Set.Finite.{u} (α := Set α) (⋃ (i : (↑{i : ι | i ∈ I} : Type u_2)), σ i)
tinter : ⋂ (i : (↑{i : ι | i ∈ I} : Type u_2)), ⋂₀ σ i ⊆ U
V : (i : (↑{i : ι | i ∈ I} : Type u_2)) → Set α := fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
hV : V = fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
mp : U = ⋂ (i : (↑I : Type u_2)), (fun (i : (↑{i : ι | i ∈ I} : Type u_2)) ↦ U ∪ ⋂₀ σ i) i
mp₁ : U = U ∪ ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i
mp₂ : U = U
mp₃ : ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i ⊆ U
mp₄ : U = U
mp₅ mp₆ mp₇ : ⋂ (i : (↑I : Type u_2)), ⋂₀ σ i ⊆ U
⊢ U = ⋂ (i : (↑I : Type u_2)), V i

Tactic:
rwa [hV, ← union_iInter, union_eq_self_of_subset_right]

Premises used: Set.union_iInter, Set.union_eq_self_of_subset_right
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : (↑I : Type u_2) → Set α
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
mem_iInf_of_iInter Ifin V_in Subset.rfl

Premises used: Filter.mem_iInf_of_iInter, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
Ifin : I.Finite
V : (↑I : Type u_2) → Set α
V_in : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
exact mem_iInf_of_iInter Ifin V_in Subset.rfl

Premises used: Filter.mem_iInf_of_iInter, Set.Subset.rfl
-- 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
⊢ 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:
simp only [mem_iInf, biInter_eq_iInter]

Premises used: Filter.mem_iInf, Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ (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

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

Premises used: Set.iInter, Set.Finite, Exists, And, And.intro, Iff.intro, Exists.intro, Subtype.val, Eq, _private.0.Filter.mem_iInf'.match_1
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
refine :
  (∃ (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
⊢ (∃ (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

Tactic:
refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
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)

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

Premises used: Set.univ, Membership.mem, dite, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
refine_1 :
  ∀ (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 : ι) (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 :
  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)
⊢ ∃ (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)

Tactic:
refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
refine_1 : (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ) ∈ s i
⊢ (fun (i : ι) ↦ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ : Set α)) i ∈ s i

Tactic:
dsimp only
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
pos : ∀ (h : i ∈ I), V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) ∈ s i
neg : i ∉ I → univ ∈ s i
⊢ (if hi : i ∈ I then V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else univ) ∈ s i

Tactic:
split_ifs
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
h : i ∈ I
⊢ V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) ∈ s i

Tactic:
hV ⟨i,_⟩

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
h : i ∉ I
⊢ univ ∈ s i

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : (↑I : Type u_2) → Set α
hV : ∀ (i : (↑I : Type u_2)), V i ∈ s (↑i : ι)
i : ι
h : i ∈ I
⊢ V (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) ∈ s i

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

Premises used: Subtype.mk, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
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

Tactic:
dif_neg hi

Premises used: dif_neg
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
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

Tactic:
exact dif_neg hi

Premises used: dif_neg
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
s : ι → Filter α
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)

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

Premises used: Subtype.coe_prop, Set.inter_univ, Set.iInter_univ, Set.biInter_eq_iInter, dif_pos, Subtype.coe_eta, Set.iInter_dite, true_and
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
⊢ Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s

Tactic:
rw [← iInf_range' (g := (·))] at hs

Premises used: iInf_range'
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
let :
  ∀ (w : Set (↑(range f) : Type u_3)),
    w.Finite →
      ∀ (V : (↑(range f) : Type u_3) → Set α) (hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)),
        (∀ i ∉ w, V i = univ) →
          s = ⋂ i ∈ w, V i →
            ∀ (hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i),
              ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
⊢ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

Tactic:
let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
right : s = ⋂ (i : ι), (V ∘ rangeFactorization f) i
⊢ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

Tactic:
use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)

Premises used: Set.rangeFactorization
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : Membership.mem (γ := Filter α) (⨅ (b : (↑(range f) : Type u_3)), (↑b : Filter α)) s
w : Set (↑(range f) : Type u_3)
left : w.Finite
V : (↑(range f) : Type u_3) → Set α
hVs : ∀ (i : (↑(range f) : Type u_3)), V i ∈ (↑i : Filter α)
left_1 : ∀ i ∉ w, V i = univ
left_2 : s = ⋂ i ∈ w, V i
hVU' : s = ⋂ (i : (↑(range f) : Type u_3)), V i
right : Eq.{u_3 + 1} (α := Set α) (⋂ (i : (↑(range f) : Type u_3)), V i) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
right₁ : Eq.{u_3 + 1} (α := Set α) (⋂ (x : ι), V (rangeFactorization f x)) (⋂ (i : ι), (V ∘ rangeFactorization f) i)
right₂ right₃ :
  Eq.{u_3 + 1} (α := Set α) (⋂ (x : ι), V (rangeFactorization f x))
    (⋂ (i : ι), (fun (x : ι) ↦ V (rangeFactorization f x)) i)
⊢ s = ⋂ (i : ι), (V ∘ rangeFactorization f) i

Tactic:
rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]

Premises used: Set.rangeFactorization_surjective, Function.comp_def, Function.Surjective.iInter_comp
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
inst : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

Tactic:
⟨exists_iInter_of_mem_iInf, ?_⟩

Premises used: Filter.exists_iInter_of_mem_iInf, Iff.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
inst : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
refine :
  (∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i) → Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) s ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

Tactic:
refine ⟨exists_iInter_of_mem_iInf, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
inst : Finite ι
α : Type u_3
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : ι), t i)

Tactic:
iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.iInter_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
ι : Sort u_2
inst : Finite ι
α : Type u_3
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : ι), t i)

Tactic:
exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.iInter_mem
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t →
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
mpr :
  (∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) →
    Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t ↔
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Tactic:
constructor