awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun (i : ι) ↦ p i ∧ q i) s

Tactic:
⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩

Premises used: Iff.mpr, Filter.HasBasis.mem_iff, _private.0.Filter.HasBasis.restrict.match_1, Membership.mem, And.left, Filter.HasBasis.mk, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
refine : ∀ (t : Set α) (ht : t ∈ l), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
⊢ l.HasBasis (fun (i : ι) ↦ p i ∧ q i) s

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
rcases : ∀ (i : ι) (hpi : p i) (hti : s i ⊆ t), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
rcases : ∀ (j : ι) (hpj : p j) (hqj : q j) (hji : s j ⊆ s i), ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t

Tactic:
⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ (i : ι), (p i ∧ q i) ∧ s i ⊆ t

Tactic:
exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
V : Set α
hV : V ∈ l
⊢ l.HasBasis (fun (i : ι) ↦ p i ∧ s i ⊆ V) s

Tactic:
h.restrict fun _i hi => (h.mem_iff.1 (inter_mem hV (h.mem_of_mem hi))).imp fun _j hj =>
    ⟨hj.1, subset_inter_iff.1 hj.2⟩

Premises used: Filter.HasBasis.mem_iff, Set.subset_inter_iff, Filter.HasBasis.restrict, Filter.inter_mem, Exists.imp, And.intro, Iff.mp, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
p : Set α → Prop
h : l.HasBasis (fun (s : Set α) ↦ s ∈ l ∧ p s) id
V : Set α
hV : V ∈ l
⊢ l.HasBasis (fun (s : Set α) ↦ s ∈ l ∧ p s ∧ s ⊆ V) id

Tactic:
simpa only [and_assoc] using h.restrict_subset hV

Premises used: Filter.HasBasis.restrict_subset, and_assoc
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι' : Sort u_5
l l' : Filter α
p' : ι' → Prop
s' : ι' → Set α
hl' : l'.HasBasis p' s'
⊢ l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l

Tactic:
⟨fun h _i' hi' => h <| hl'.mem_of_mem hi', fun h _s hs =>
    let ⟨_i', hi', hs⟩ := hl'.mem_iff.1 hs
    mem_of_superset (h _ hi') hs⟩

Premises used: Filter.HasBasis.mem_iff, Membership.mem, Iff.intro, Iff.mp, _private.0.Filter.HasBasis.to_hasBasis'.match_1, Filter.HasBasis.mem_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ l ≤ l' ↔ ∀ t ∈ l', ∃ (i : ι), p i ∧ s i ⊆ t

Tactic:
simp only [le_def, hl.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.le_def
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'

Tactic:
simp only [hl'.ge_iff, hl.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.ge_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = ⊤ ↔ ∀ (i : ι), p i → s i = univ

Tactic:
simp [← top_le_iff, h.ge_iff]

Premises used: Filter.HasBasis.ge_iff, top_le_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
a : l ≤ l'
a₁ : l' ≤ l
⊢ l = l'

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' a : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
⊢ l ≤ l'

Tactic:
rw [hl.le_basis_iff hl']

Premises used: Filter.HasBasis.le_basis_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'

Tactic:
simpa using h'
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
a : ∀ (i' : ι), p i' → ∃ (i : ι'), p' i ∧ s' i ⊆ s i'
⊢ l' ≤ l

Tactic:
rw [hl'.le_basis_iff hl]

Premises used: Filter.HasBasis.le_basis_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ (i : ι), p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ (i : ι'), p' i ∧ s' i ⊆ s i'

Tactic:
simpa using h
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
mp : t ∈ l ⊓ l' → ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
mpr : (∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
⊢ t ∈ l ⊓ l' ↔ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
mp :
  (∃ (t₁ : Set α), (∃ (i : ι), p i ∧ s i ⊆ t₁) ∧ ∃ (t₂ : Set α), (∃ (i : ι'), p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
    ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
⊢ t ∈ l ⊓ l' → ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.mem_inf_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'

Tactic:
⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩

Premises used: PProd.mk, Set.inter_subset_inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'

Tactic:
exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
i' : ι'
H : s ⟨i, i'⟩.fst ∩ s' ⟨i, i'⟩.snd ⊆ t
hi : p ⟨i, i'⟩.fst
hi' : p' ⟨i, i'⟩.snd
⊢ t ∈ l ⊓ l'

Tactic:
mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H

Premises used: Filter.mem_inf_of_inter, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
i' : ι'
H : s ⟨i, i'⟩.fst ∩ s' ⟨i, i'⟩.snd ⊆ t
hi : p ⟨i, i'⟩.fst
hi' : p' ⟨i, i'⟩.snd
⊢ t ∈ l ⊓ l'

Tactic:
exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H

Premises used: Filter.mem_inf_of_inter, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l l' : Filter α
ι : Type u_6
ι' : Type u_7
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ (l ⊓ l').HasBasis (fun (i : ι × ι') ↦ p i.1 ∧ p' i.2) fun (i : ι × ι') ↦ s i.1 ∩ s' i.2

Tactic:
(hl.inf' hl').comp_equiv Equiv.pprodEquivProd.symm

Premises used: Filter.HasBasis.inf', Filter.HasBasis.comp_equiv, Equiv.pprodEquivProd, Equiv.symm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (ii' : (i : ι) × ι' i) ↦ p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))

Tactic:
⟨fun t => ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
refine :
  ∀ (t : Set α),
    Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
      ∃ (i : (i : ι) × ι' i),
        p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ∧
          s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
⊢ HasBasis (α := α) (⨅ (i : ι), l i)
    (fun (ii' : (i : ι) × ι' i) ↦ p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))

Tactic:
refine ⟨fun t => ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
rw :
  (∃ (i : ι), t ∈ l i) ↔
    ∃ (a : ι) (b : ι' a),
      p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ∧
        s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
          t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Sigma.exists]

Premises used: Sigma.exists, Filter.mem_iInf_of_directed
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ (i : ι), t ∈ l i) ↔
    ∃ (a : ι) (b : ι' a),
      p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ∧
        s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
          t

Tactic:
exists_congr fun i => (hl i).mem_iff

Premises used: Filter.HasBasis.mem_iff, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ (i : ι), t ∈ l i) ↔
    ∃ (a : ι) (b : ι' a),
      p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
          ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ∧
        s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
          t

Tactic:
exact exists_congr fun i => (hl i).mem_iff

Premises used: Filter.HasBasis.mem_iff, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
⊢ HasBasis (α := α) (⨅ (i : ι), l i) (fun (ii' : ι × ι') ↦ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦ s ii'.1 ii'.2

Tactic:
⟨fun t => ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
refine : ∀ (t : Set α), Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔ ∃ (i : ι × ι'), p i.1 i.2 ∧ s i.1 i.2 ⊆ t
⊢ HasBasis (α := α) (⨅ (i : ι), l i) (fun (ii' : ι × ι') ↦ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦ s ii'.1 ii'.2

Tactic:
refine ⟨fun t => ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
rw : (∃ (i : ι), t ∈ l i) ↔ ∃ (a : ι) (b : ι'), p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔ ∃ (i : ι × ι'), p i.1 i.2 ∧ s i.1 i.2 ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Prod.exists]

Premises used: Filter.mem_iInf_of_directed, Prod.exists
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ (i : ι), t ∈ l i) ↔ ∃ (a : ι) (b : ι'), p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t

Tactic:
exists_congr fun i => (hl i).mem_iff

Premises used: Filter.HasBasis.mem_iff, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ (i : ι), t ∈ l i) ↔ ∃ (a : ι) (b : ι'), p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t

Tactic:
exact exists_congr fun i => (hl i).mem_iff

Premises used: Filter.HasBasis.mem_iff, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i)
    (fun (ii' : (i : ι) × ι' i) ↦
      ii'.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
        p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))

Tactic:
⟨fun t => ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
refine :
  ∀ (t : Set α),
    Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔
      ∃ (i : (i : ι) × ι' i),
        (i.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
            p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i))) ∧
          s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i)
    (fun (ii' : (i : ι) × ι' i) ↦
      ii'.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
        p (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i)))
    fun (ii' : (i : ι) × ι' i) ↦ s (ii'.fst (β := fun (i : ι) ↦ ι' i)) (ii'.snd (β := fun (i : ι) ↦ ι' i))

Tactic:
refine ⟨fun t => ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
rw :
  (∃ i ∈ dom, t ∈ l i) ↔
    ∃ (a : ι) (b : ι' a),
      ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
          p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i))) ∧
        s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
          t
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔
    ∃ (i : (i : ι) × ι' i),
      (i.fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧ p (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i))) ∧
        s (i.fst (β := fun (i : ι) ↦ ι' i)) (i.snd (β := fun (i : ι) ↦ ι' i)) ⊆ t

Tactic:
rw [mem_biInf_of_directed h hdom, Sigma.exists]

Premises used: Sigma.exists, Filter.mem_biInf_of_directed
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔
    ∃ (a : ι) (b : ι' a),
      ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i) ∈ dom ∧
          p ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i))) ∧
        s ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).fst (β := fun (i : ι) ↦ ι' i))
            ((Sigma.mk (β := fun (a : ι) ↦ ι' a) a b).snd (β := fun (i : ι) ↦ ι' i)) ⊆
          t

Tactic:
grind +splitIndPred
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i) (fun (ii' : ι × ι') ↦ ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦
    s ii'.1 ii'.2

Tactic:
⟨fun t => ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
refine :
  ∀ (t : Set α),
    Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔ ∃ (i : ι × ι'), (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t
⊢ HasBasis (α := α) (⨅ i ∈ dom, l i) (fun (ii' : ι × ι') ↦ ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun (ii' : ι × ι') ↦
    s ii'.1 ii'.2

Tactic:
refine ⟨fun t => ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
rw : (∃ i ∈ dom, t ∈ l i) ↔ ∃ (a : ι) (b : ι'), ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ dom, l i) t ↔ ∃ (i : ι × ι'), (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t

Tactic:
rw [mem_biInf_of_directed h hdom, Prod.exists]

Premises used: Filter.mem_biInf_of_directed, Prod.exists
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ (a : ι) (b : ι'), ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t

Tactic:
grind +splitIndPred
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
U : Set α
⊢ Membership.mem (γ := Filter α) ⊤ U ↔ ∃ (i : Unit), True ∧ univ ⊆ U

Tactic:
simp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
t U : Set α
⊢ U ∈ 𝓟 t ↔ ∃ (i : Unit), True ∧ t ⊆ U

Tactic:
simp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
x : α
⊢ HasBasis (pure x) (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}

Tactic:
simp only [← principal_singleton, hasBasis_principal]

Premises used: Filter.principal_singleton, Filter.hasBasis_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
simp_rw :
  (∃ (x : ι) (x_1 : ι'), (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ (a : ι) (b : ι'), (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
⊢ t ∈ l ⊔ l' ↔ ∃ (i : ι ×' ι'), (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]

Premises used: Filter.HasBasis.mem_iff, Set.union_subset_iff, PProd.exists, exists_and_left, exists_and_right, Filter.mem_sup
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ (x : ι) (x_1 : ι'), (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ (a : ι) (b : ι'), (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t

Tactic:
simp only [and_assoc, and_left_comm]

Premises used: and_left_comm, and_assoc
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l l' : Filter α
ι : Type u_6
ι' : Type u_7
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ (l ⊔ l').HasBasis (fun (i : ι × ι') ↦ p i.1 ∧ p' i.2) fun (i : ι × ι') ↦ s i.1 ∪ s' i.2

Tactic:
(hl.sup' hl').comp_equiv Equiv.pprodEquivProd.symm

Premises used: Filter.HasBasis.comp_equiv, Equiv.pprodEquivProd, Equiv.symm, Filter.HasBasis.sup'