awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
refine_1 :
  ∀ (t : Set α) (ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t),
    ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
      (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
          ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
        ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
          t
refine_2 :
  ∀ (t : Set α),
    (∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
        (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
            ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
              p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
          ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
              s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
            t) →
      Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
      If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i))
    fun (If : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
      s (↑i : ι) (If.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i)

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
refine_1 :
  ∀ (I : Set ι) (f : (i : ι) → ι' i) (hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t) (hI : (I, f).1.Finite)
    (hf : ∀ i ∈ (I, f).1, p i ((I, f).2 i)),
    ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
      (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
          ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
        ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
            s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
          t
⊢ ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t

Tactic:
rcases (HasBasis.iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.iInf', Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI : (I, f).1.Finite
hf : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t

Tactic:
⟨⟨I, fun i => f i⟩, ⟨hI, Subtype.forall.mpr hf⟩, trans (iInter_subtype _ _) hsub⟩

Premises used: Iff.mpr, Trans.trans, Subtype.forall, Set.iInter_subtype, And.intro, Exists.intro, Sigma.mk, Subtype.val
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI : (I, f).1.Finite
hf : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ ∃ (i : (I : Set ι) × ((i : (↑I : Type u_6)) → ι' (↑i : ι))),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          p (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1)) ∧
      ⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))) : Type u_6)),
          s (↑i_1 : ι) (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) i_1) ⊆
        t

Tactic:
exact ⟨⟨I, fun i => f i⟩, ⟨hI, Subtype.forall.mpr hf⟩, trans (iInter_subtype _ _) hsub⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
refine_2 :
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t

Tactic:
grw [← hsub]
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
refine_2 :
  ∀
    (val :
      Fintype
        (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
              (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
          Type u_6)),
    Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
      (⋂ (i :
        (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
              (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
          Type u_6)),
        s (↑i : ι)
          (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))

Tactic:
cases hI.nonempty_fintype

Premises used: Set.Finite.nonempty_fintype
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
val :
  Fintype
    (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
      Type u_6)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))

Tactic:
iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.iInter_mem
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : (↑I : Type u_6)) → ι' (↑i : ι)
hsub :
  ⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i) ⊆
    t
hI :
  (Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
      (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)).Finite
hf :
  ∀
    (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
    p (↑i : ι)
      (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
        (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i)
val :
  Fintype
    (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
      Type u_6)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i)
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f)) :
        Type u_6)),
      s (↑i : ι)
        (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι))
          (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_6)) → ι' (↑i : ι)) I f) i))

Tactic:
exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.iInter_mem
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
rcases :
  ∀ (t : I → Set α) (htl : ∀ (i : I), t i ∈ l i) (hd : Pairwise (Disjoint on t)),
    ∃ (ind : (i : I) → ι i),
      (∀ (i : I), p i (ind i)) ∧
        Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))

Tactic:
rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩

Premises used: Pairwise.exists_mem_filter_of_disjoint
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd_1 : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
choose :
  ∀ (ind : (i : I) → ι i) (hp : ∀ (i : I), p i (ind i)) (ht : ∀ (i : I), s i (ind i) ⊆ t i),
    ∃ (ind : (i : I) → ι i),
      (∀ (i : I), p i (ind i)) ∧
        Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd_1 : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))

Tactic:
⟨ind, hp, hd.mono fun i j hij => hij.mono (ht _) (ht _)⟩

Premises used: And.intro, Exists.intro, Disjoint.mono, Pairwise.mono
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_7
inst : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd_1 : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧
      Pairwise.{u_7} (α := I) (Function.onFun.{u_7 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : I) ↦ s i (ind i))

Tactic:
exact ⟨ind, hp, hd.mono fun i j hij => hij.mono (ht _) (ht _)⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
rcases :
  ∀ (t : I → Set α) (htl : ∀ (i : I), t i ∈ l i) (hd : S.PairwiseDisjoint t),
    ∃ (ind : (i : I) → ι i),
      (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)

Tactic:
rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩

Premises used: Set.PairwiseDisjoint.exists_mem_filter
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd_1 : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
choose :
  ∀ (ind : (i : I) → ι i) (hp : ∀ (i : I), p i (ind i)) (ht : ∀ (i : I), s i (ind i) ⊆ t i),
    ∃ (ind : (i : I) → ι i),
      (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd_1 : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)

Tactic:
⟨ind, hp, hd.mono ht⟩

Premises used: Set.PairwiseDisjoint.mono, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd_1 : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ (ind : (i : I) → ι i),
    (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint.{u_1, u_6} (α := Set α) S fun (i : I) ↦ s i (ind i)

Tactic:
exact ⟨ind, hp, hd.mono ht⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
s : ι → Set α
⊢ HasBasis.{u_1, u_6 + 1} (α := α) (⨅ (i : ι), 𝓟 (s i)) (fun (t : Set ι) ↦ t.Finite) fun (t : Set ι) ↦ ⋂ i ∈ t, s i

Tactic:
⟨fun U => (mem_iInf_finite _).trans ?_⟩

Premises used: Filter.mem_iInf_finite, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
s : ι → Set α
refine :
  ∀ (U : Set α),
    (∃ (t : Finset ι), Membership.mem (γ := Filter α) (⨅ i ∈ t, 𝓟 (s i)) U) ↔
      ∃ (i : Set ι), i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U
⊢ HasBasis.{u_1, u_6 + 1} (α := α) (⨅ (i : ι), 𝓟 (s i)) (fun (t : Set ι) ↦ t.Finite) fun (t : Set ι) ↦ ⋂ i ∈ t, s i

Tactic:
refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
ι : Type u_6
s : ι → Set α
U : Set α
⊢ (∃ (t : Finset ι), Membership.mem (γ := Filter α) (⨅ i ∈ t, 𝓟 (s i)) U) ↔
    ∃ (i : Set ι), i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U

Tactic:
simp only [iInf_principal_finset, mem_principal,
    exists_finite_iff_finset, Finset.set_biInter_coe]

Premises used: Filter.iInf_principal_finset, Finset.set_biInter_coe, Filter.mem_principal, Set.exists_finite_iff_finset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ f = g ↔ f.sets = g.sets

Tactic:
⟨congr_arg _, filter_eq⟩

Premises used: congr_arg, Iff.intro, Filter.filter_eq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ f.sets ⊆ g.sets ↔ g ≤ f

Tactic:
.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ f.sets ⊂ g.sets ↔ g < f

Tactic:
.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
h : ∀ (s : Set α), sᶜ ∈ f ↔ sᶜ ∈ g
⊢ f = g

Tactic:
Filter.ext <| compl_surjective.forall.2 h

Premises used: Iff.mpr, Function.Surjective.forall, Filter.ext, compl_surjective
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
⊢ s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f

Tactic:
⟨fun h => ⟨mem_of_superset h inter_subset_left, mem_of_superset h inter_subset_right⟩,
    and_imp.2 inter_mem⟩

Premises used: Iff.mpr, and_imp, Filter.inter_mem, Set.inter_subset_left, And.intro, Iff.intro, Set.inter_subset_right, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
hs : s ∈ f
ht : tᶜ ∈ f
⊢ s \ t ∈ f

Tactic:
inter_mem hs ht

Premises used: Set.Mem, Set.diff, Filter.inter_mem, setOf, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
h : {x : α | x ∈ s ↔ x ∈ t} ∈ f
⊢ s ∈ f ↔ t ∈ f

Tactic:
⟨fun hs => mp_mem hs (mem_of_superset h fun _ => Iff.mp), fun hs =>
    mp_mem hs (mem_of_superset h fun _ => Iff.mpr)⟩

Premises used: Iff.mpr, Filter.mp_mem, Iff.intro, Iff.mp, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
S : Set (Set α)
hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f
⊢ f.copy S hmem = f

Tactic:
Filter.ext hmem

Premises used: Filter.ext
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
he : ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
h₁ :
  ∀ (x : β),
    ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) {x} i), s i ∈ f ↔
      ∀ (i : β), Membership.mem (γ := Set β) {x} i → s i ∈ f
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
apply Subsingleton.induction_on hf

Premises used: Set.Subsingleton.induction_on
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ∀ (x : β),
    ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) {x} i), s i ∈ f ↔
      ∀ (i : β), Membership.mem (γ := Set β) {x} i → s i ∈ f

Tactic:
simp