awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
mp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : (↑I : Type u_2) → Set α),
          (∀ (i : (↑I : Type u_2)),
              ∃ (t : p (↑i : ι) → Set α), (∀ (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i_1) ∧ V i = ⋂ (i : p (↑i : ι)), t i) ∧
            t = ⋂ (i : (↑I : Type u_2)), V i) →
    ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ 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:
simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]

Premises used: Filter.mem_iInf, Filter.mem_principal, Filter.mem_iInf_of_finite
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
hV₁ :
  ∀ (i : (↑I : Type u_2)),
    ∃ (t : p (↑i : ι) → Set α), (∀ (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i_1) ∧ V i = ⋂ (i : p (↑i : ι)), t i
mp :
  ∀ (t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α)
    (ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1)
    (ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1),
    ∃ (I_1 : Set ι),
      I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
choose! t ht₁ ht₂ using hV₁
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩

Premises used: Set.Finite.inter_of_left, setOf, Inter.inter, And.right, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
mp : Subset.{u} (α := Set α) (⋂ i ∈ I ∩ {i : ι | p i}, s i) (⋂ (i : (↑I : Type u_2)), V i)
⊢ ∃ (I_1 : Set ι),
    I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ Subset.{u} (α := Set α) (⋂ i ∈ I_1, s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
mp :
  Subset.{u} (α := Set α) (⋂ (x : (↑I : Type u_2)), ⋂ (_ : p (↑x : ι)), s (↑x : ι))
    (⋂ (i : (↑I : Type u_2)), ⋂ (i_1 : p (↑i : ι)), t i i_1)
⊢ Subset.{u} (α := Set α) (⋂ i ∈ I ∩ {i : ι | p i}, s i) (⋂ (i : (↑I : Type u_2)), V i)

Tactic:
simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_setOf_eq]

Premises used: Set.mem_inter_iff, Set.biInter_eq_iInter, Set.mem_setOf_eq, Set.iInter_and
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
mp : ∀ (i : (↑I : Type u_2)) (hpi : p (↑i : ι)), s (↑i : ι) ⊆ t i hpi
⊢ Subset.{u} (α := Set α) (⋂ (x : (↑I : Type u_2)), ⋂ (_ : p (↑x : ι)), s (↑x : ι))
    (⋂ (i : (↑I : Type u_2)), ⋂ (i_1 : p (↑i : ι)), t i i_1)

Tactic:
gcongr with i hpi
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
i : (↑I : Type u_2)
hpi : p (↑i : ι)
⊢ s (↑i : ι) ⊆ t i hpi

Tactic:
ht₁ i hpi
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : (↑I : Type u_2) → Set α
t : (i : (↑I : Type u_2)) → p (↑i : ι) → Set α
ht₁ : ∀ (i : (↑I : Type u_2)) (i_1 : p (↑i : ι)), s (↑i : ι) ⊆ t i i_1
ht₂ : ∀ (i : (↑I : Type u_2)), V i = ⋂ (i_1 : p (↑i : ι)), t i i_1
i : (↑I : Type u_2)
hpi : p (↑i : ι)
⊢ s (↑i : ι) ⊆ t i hpi

Tactic:
exact ht₁ i hpi
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ i ∈ I, s i ⊆ t
⊢ ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t

Tactic:
rw [biInter_eq_iInter] at hst

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t

Tactic:
mem_iInf_of_iInter hIf (fun i ↦ ?_) hst

Premises used: Filter.mem_iInf_of_iInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t
mpr : ∀ (i : (↑I : Type u_2)), Membership.mem (γ := Filter α) (⨅ (_ : p (↑i : ι)), 𝓟 (s (↑i : ι))) (s (↑i : ι))
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) t

Tactic:
refine mem_iInf_of_iInter hIf (fun i ↦ ?_) hst

Premises used: Filter.mem_iInf_of_iInter
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ (x : (↑I : Type u_2)), s (↑x : ι) ⊆ t
i : (↑I : Type u_2)
⊢ Membership.mem (γ := Filter α) (⨅ (_ : p (↑i : ι)), 𝓟 (s (↑i : ι))) (s (↑i : ι))

Tactic:
simp [hpI i i.2]

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ Pairwise fun (i j : ι) ↦
    ∃ (s : { s : Set α // s ∈ l i }) (t : { t : Set α // t ∈ l j }), Disjoint (↑s : Set α) (↑t : Set α)

Tactic:
simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd

Premises used: Function.onFun, Filter.disjoint_iff, Subtype.exists, exists_prop, Pairwise
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ Pairwise fun (i j : ι) ↦
    ∃ (s : { s : Set α // s ∈ l i }) (t : { t : Set α // t ∈ l j }), Disjoint (↑s : Set α) (↑t : Set α)

Tactic:
have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
    simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this :
  Pairwise fun (i j : ι) ↦
    ∃ (s : { s : Set α // s ∈ l i }) (t : { t : Set α // t ∈ l j }), Disjoint (↑s : Set α) (↑t : Set α)
choose! :
  ∀ (s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }) (t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j })
    (hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)),
    ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
choose! s t hst using this
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩

Premises used: Set.iInter, Inter.inter, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
refine_1 : ∀ (i : ι), (fun (i : ι) ↦ (⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α) : Set α)) i ∈ l i
refine_2 :
  ∀ (i j : ι) (hij : i ≠ j),
    onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint
      (fun (i : ι) ↦ ⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α)) i j
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
i : ι
⊢ (fun (i : ι) ↦ (⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α) : Set α)) i ∈ l i

Tactic:
iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2

Premises used: Iff.mpr, Set.Mem, Filter.inter_mem, Filter.iInter_mem, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
i j : ι
hij : i ≠ j
⊢ onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint
    (fun (i : ι) ↦ ⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α)) i j

Tactic:
(hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
      ((iInter_subset _ i).trans inter_subset_right)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.iInter_subset, Disjoint.mono, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
inst : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i j : ι⦄ → { s : Set α // s ∈ l i }
t : ⦃i j : ι⦄ → { t : Set α // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint (↑(s (j := j)) : Set α) (↑(t (i := i)) : Set α)
i : ι
⊢ (fun (i : ι) ↦ (⋂ (j : ι), (↑(s (j := j)) : Set α) ∩ (↑(t (i := j)) : Set α) : Set α)) i ∈ l i

Tactic:
exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
    (hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
      ((iInter_subset _ i).trans inter_subset_right)]

Premises used: Iff.mpr, Filter.inter_mem, Filter.iInter_mem, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
⊢ Finite.{u_2 + 1} (↑t : Type u_2)

Tactic:
haveI := ht.to_subtype
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
rcases :
  ∀ (s : (↑t : Type u_2) → Set α) (hsl : ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)) (hsd : Pairwise (Disjoint on s)),
    ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩

Premises used: Set.Pairwise.subtype, Pairwise.exists_mem_filter_of_disjoint
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (↑t : Type u_2) → Set α
hsl : ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)
hsd : Pairwise (Disjoint on s)
⊢ ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)

Tactic:
hsl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (↑t : Type u_2) → Set α
hsl : ∀ (i : (↑t : Type u_2)), s i ∈ l (↑i : ι)
hsd : Pairwise (Disjoint on s)
lift :
  ∀ (s : (i : (↑t : Type u_2)) → { s : Set α // s ∈ l (↑i : ι) })
    (hsd :
      Pairwise.{u_2} (α := (↑t : Type u_2))
        (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦ (↑(s i) : Set α))),
    ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
lift s to (i : t) → {s // s ∈ l i} using hsl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (i : (↑t : Type u_2)) → { s : Set α // s ∈ l (↑i : ι) }
hsd :
  Pairwise.{u_2} (α := (↑t : Type u_2))
    (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦ (↑(s i) : Set α))
rcases :
  ∀ (s : (i : ι) → { s : Set α // s ∈ l i })
    (hsd :
      Pairwise.{u_2} (α := (↑t : Type u_2))
        (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦
          (↑((fun (i : { x : ι // x ∈ t }) ↦ (s (↑i : ι) : { s : Set α // s ∈ l (↑i : ι) })) i) : Set α))),
    ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩

Premises used: Subtype.exists_pi_extension, rfl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (i : ι) → { s : Set α // s ∈ l i }
hsd :
  Pairwise.{u_2} (α := (↑t : Type u_2))
    (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦
      (↑((fun (i : { x : ι // x ∈ t }) ↦ (s (↑i : ι) : { s : Set α // s ∈ l (↑i : ι) })) i) : Set α))
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩

Premises used: Pairwise.set_of_subtype, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite.{u_2 + 1} (↑t : Type u_2)
s : (i : ι) → { s : Set α // s ∈ l i }
hsd :
  Pairwise.{u_2} (α := (↑t : Type u_2))
    (onFun.{u_2 + 1, u + 1, 1} (β := Set α) Disjoint fun (i : (↑t : Type u_2)) ↦
      (↑((fun (i : { x : ι // x ∈ t }) ↦ (s (↑i : ι) : { s : Set α // s ∈ l (↑i : ι) })) i) : Set α))
⊢ ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (t : Finset ι) ↦ ⨅ i ∈ t, f i
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset ι), sets (⨅ i ∈ t, f i))

Tactic:
rw [iInf_eq_iInf_finset, iInf_sets_eq]

Premises used: Filter.iInf_sets_eq, iInf_eq_iInf_finset
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (t : Finset ι) ↦ ⨅ i ∈ t, f i

Tactic:
directed_of_isDirected_le fun _ _ => biInf_mono

Premises used: directed_of_isDirected_le, biInf_mono
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (t : Finset ι) ↦ ⨅ i ∈ t, f i

Tactic:
exact directed_of_isDirected_le fun _ _ => biInf_mono

Premises used: directed_of_isDirected_le
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
rw : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (sets (⨅ (i : PLift ι), f i.down))
rw₁ :
  Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (x : PLift ι), f ((Equiv.plift : (a : PLift ι) → ι) x)))
    (sets (⨅ (i : PLift ι), f i.down))
rw₂ rw₃ : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (x : PLift ι), f x.down)) (sets (⨅ (i : PLift ι), f i.down))
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset (PLift ι)), sets (⨅ i ∈ t, f i.down))

Tactic:
rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]

Premises used: Equiv.plift_apply, Filter.iInf_sets_eq_finite, Equiv.plift, Function.Surjective.iInf_comp, Equiv.surjective
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Type u_2
f : ι → Filter α
s : Set α
⊢ s ∈ iInf f ↔ ∃ (t : Finset ι), Membership.mem (γ := Filter α) (⨅ i ∈ t, f i) s

Tactic:
(Set.ext_iff.1 (iInf_sets_eq_finite f) s).trans mem_iUnion

Premises used: Set.Mem, setOf, Set.mem_iUnion, Filter.iInf_sets_eq_finite, Iff.mp, Iff.trans, Set.ext_iff
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
⊢ s ∈ iInf f ↔ ∃ (t : Finset (PLift ι)), Membership.mem (γ := Filter α) (⨅ i ∈ t, f i.down) s

Tactic:
(Set.ext_iff.1 (iInf_sets_eq_finite' f) s).trans mem_iUnion

Premises used: Set.Mem, Filter.iInf_sets_eq_finite', setOf, Set.mem_iUnion, Iff.mp, Iff.trans, Set.ext_iff
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
simp :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']

Premises used: Finset.set_biInter_coe, Set.biInter_eq_iInter, iInf_subtype'
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
refine_1 :
  ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
refine_2 :
  (∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)) →
    Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
refine_1 :
  ∀ (p : Subtype (Membership.mem s) → Set β) (hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α))
    (h :
      Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
        (⋂ (i : Subtype (Membership.mem s)), p i)),
    ∃ (p_1 : α → Set β),
      (∀ a ∈ s, p_1 a ∈ f a) ∧
        Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
          (⋂ (x : (↑(↑s : Set α) : Type u)), p_1 (↑x : α))
⊢ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)

Tactic:
rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩

Premises used: Iff.mp, Filter.mem_iInf_of_finite, rfl
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
a : α
ha : a ∈ s
⊢ (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) a ∈ f a

Tactic:
simpa [ha] using hp ⟨a, ha⟩

Premises used: Subtype.mk
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
refine_1 :
  Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
    (⋂ (x : (↑(↑s : Set α) : Type u)),
      (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑x : α))
⊢ ∃ (p_1 : α → Set β),
    (∀ a ∈ s, p_1 a ∈ f a) ∧
      Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i) (⋂ (x : (↑(↑s : Set α) : Type u)), p_1 (↑x : α))

Tactic:
refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
⊢ Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
    (⋂ (x : (↑(↑s : Set α) : Type u)),
      (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑x : α))

Tactic:
iInter_congr_of_surjective id surjective_id ?_

Premises used: id, Function.surjective_id, Set.iInter_congr_of_surjective
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
refine_1 :
  ∀ (x : Subtype (Membership.mem s)),
    (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑(id x) : α) = p x
⊢ Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
    (⋂ (x : (↑(↑s : Set α) : Type u)),
      (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑x : α))

Tactic:
refine iInter_congr_of_surjective id surjective_id ?_

Premises used: id, Function.surjective_id, Set.iInter_congr_of_surjective
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
a : α
ha : a ∈ s
⊢ (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β))
      (↑(id (Subtype.mk (p := Membership.mem s) a ha)) : α) =
    p (Subtype.mk (p := Membership.mem s) a ha)

Tactic:
simp [ha]
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ a ∈ s, p a ∈ f a
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α))

Tactic:
iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.iInter_mem, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Filter.Finite
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ a ∈ s, p a ∈ f a
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α))

Tactic:
exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)