awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
ι : Type u_6
ι' : Type u_7
pa : ι → Prop
sa : ι → Set α
pb : ι' → Prop
sb : ι' → Set β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ (la ×ˢ lb).HasBasis (fun (i : ι × ι') ↦ pa i.1 ∧ pb i.2) fun (i : ι × ι') ↦ sa i.1 ×ˢ sb i.2

Tactic:
(hla.comap Prod.fst).inf (hlb.comap Prod.snd)

Premises used: Filter.HasBasis.inf, Set.Mem, setOf, Set.prod, Prod.fst, Filter.HasBasis.comap, Set.preimage, Prod.snd
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 sa ×ˢ lb).HasBasis pb fun (x : ι') ↦ sa ×ˢ sb x

Tactic:
simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.snd).principal_inf _

Premises used: Filter.prod_eq_inf, Set.prod_eq, Filter.HasBasis.comap, Filter.HasBasis.principal_inf, Filter.comap_principal, Prod.snd
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
sb : Set β
⊢ (la ×ˢ 𝓟 sb).HasBasis pa fun (x : ι) ↦ sa x ×ˢ sb

Tactic:
simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.fst).inf_principal _

Premises used: Filter.prod_eq_inf, Set.prod_eq, Prod.fst, Filter.HasBasis.comap, Filter.comap_principal, Filter.HasBasis.inf_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (SProd.sprod (α := Filter α) ⊤ lb).HasBasis pb fun (x : ι') ↦ SProd.sprod (α := Set α) univ (sb x)

Tactic:
simpa only [principal_univ] using h.principal_prod univ

Premises used: Set.univ, Filter.principal_univ, Filter.HasBasis.principal_prod
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
⊢ (SProd.sprod (β := Filter β) la ⊤).HasBasis pa fun (x : ι) ↦ SProd.sprod (β := Set β) (sa x) univ

Tactic:
simpa only [principal_univ] using h.prod_principal univ

Premises used: Set.univ, Filter.HasBasis.prod_principal, Filter.principal_univ
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
simp :
  ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
⊢ (la ×ˢ lb).HasBasis p fun (i : ι) ↦ sa i ×ˢ sb i

Tactic:
simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.hasBasis_iff, Filter.HasBasis.prod_pprod
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t

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

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
refine_1 :
  ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
refine_2 :
  ∀ (t : Set (α × β)),
    (∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
⊢ ∀ (t : Set (α × β)),
    (∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t

Tactic:
refine fun t => ⟨?_, ?_⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
refine_1 :
  ∀ (k : ι) (hk : p k) (ki : sa k ⊆ sa ⟨i, j⟩.fst) (kj : sb k ⊆ sb ⟨i, j⟩.snd), ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t
⊢ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t

Tactic:
rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
k : ι
hk : p k
ki : sa k ⊆ sa ⟨i, j⟩.fst
kj : sb k ⊆ sb ⟨i, j⟩.snd
⊢ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t

Tactic:
⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, Set.prod_mono
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
k : ι
hk : p k
ki : sa k ⊆ sa ⟨i, j⟩.fst
kj : sb k ⊆ sb ⟨i, j⟩.snd
⊢ ∃ (i : ι), p i ∧ sa i ×ˢ sb i ⊆ t

Tactic:
exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i : ι
hi : p i
h : sa i ×ˢ sb i ⊆ t
⊢ ∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t

Tactic:
⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩

Premises used: PProd.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i : ι
hi : p i
h : sa i ×ˢ sb i ⊆ t
⊢ ∃ (i : ι ×' ι), (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t

Tactic:
exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
ι : Type u_6
inst : LinearOrder ι
p : ι → Prop
sa : ι → Set α
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
hsa : MonotoneOn sa {i : ι | p i}
hsb : MonotoneOn sb {i : ι | p i}
⊢ (la ×ˢ lb).HasBasis p fun (i : ι) ↦ sa i ×ˢ sb i

Tactic:
hla.prod_same_index hlb fun {i j} hi hj =>
    have : p (min i j) := min_rec' _ hi hj
    ⟨min i j, this, hsa this hi <| min_le_left _ _, hsb this hj <| min_le_right _ _⟩

Premises used: min_le_left, And.intro, min_le_right, Exists.intro, min_rec', Min.min, Filter.HasBasis.prod_same_index
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
ι : Type u_6
inst : LinearOrder ι
p : ι → Prop
sa : ι → Set α
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
hsa : AntitoneOn sa {i : ι | p i}
hsb : AntitoneOn sb {i : ι | p i}
⊢ (la ×ˢ lb).HasBasis p fun (i : ι) ↦ sa i ×ˢ sb i

Tactic:
@HasBasis.prod_same_index_mono _ _ _ _ ιᵒᵈ _ _ _ _ hla hlb hsa.dual_left hsb.dual_left

Premises used: Filter.HasBasis.prod_same_index_mono, AntitoneOn.dual_left, OrderDual
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ (k : ι), pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
simpa only [exists_prop, subset_inter_iff] using
      hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

Premises used: Filter.HasBasis.mem_iff, Set.subset_inter_iff, Filter.inter_mem, exists_prop, Iff.mp, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
la : Filter α
s : Set (α × α)
⊢ s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s

Tactic:
la.basis_sets.prod_self.mem_iff

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.prod_self, Filter.basis_sets
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
la : Filter α
r : α → α → Prop
⊢ (∃ t ∈ la, t ×ˢ t ⊆ {x : α × α | (fun (x : α × α) ↦ r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

Tactic:
simp only [prod_subset_iff, mem_setOf_eq]

Premises used: Set.prod_subset_iff, Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
la : Filter α
r : α × α → Prop
⊢ (∀ᶠ (x : α × α) in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y)

Tactic:
Iff.symm eventually_prod_self_iff.symm

Premises used: Filter.eventually_prod_self_iff, Iff.symm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_6
inst : LinearOrder ι
f : Filter α
g : Filter β
s : ι → Set α
t : ι → Set β
hf : f.HasAntitoneBasis s
hg : g.HasAntitoneBasis t
⊢ (f ×ˢ g).HasAntitoneBasis fun (n : ι) ↦ s n ×ˢ t n

Tactic:
⟨hf.1.prod_same_index_anti hg.1 (hf.2.antitoneOn _) (hg.2.antitoneOn _), hf.2.set_prod hg.2⟩

Premises used: Filter.HasAntitoneBasis.toHasBasis, Antitone.antitoneOn, Antitone.set_prod, Filter.HasAntitoneBasis.mk, Filter.HasBasis.prod_same_index_anti, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
ι : Type u_6
ι' : Type u_7
pa : ι → Prop
sa : ι → Set α
pb : ι' → Prop
sb : ι' → Set β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ (la.coprod lb).HasBasis (fun (i : ι × ι') ↦ pa i.1 ∧ pb i.2) fun (i : ι × ι') ↦
    Prod.fst ⁻¹' sa i.1 ∪ Prod.snd ⁻¹' sb i.2

Tactic:
(hla.comap Prod.fst).sup (hlb.comap Prod.snd)

Premises used: Set.Mem, setOf, Prod.fst, Filter.HasBasis.comap, Filter.coprod, Prod.snd, Filter.HasBasis.sup
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk (β := π) a) (comap (g a) l) =
    comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)

Tactic:
(((basis_sets _).comap _).map _).eq_of_same_basis ?_

Premises used: Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
refine :
  (comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)).HasBasis
    (fun (s : Set (π' (f a))) ↦ s ∈ l) fun (i : Set (π' (f a))) ↦ Sigma.mk (β := π) a '' g a ⁻¹' id i
⊢ map (Sigma.mk (β := π) a) (comap (g a) l) =
    comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)

Tactic:
refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_

Premises used: Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ (comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)).HasBasis
    (fun (s : Set (π' (f a))) ↦ s ∈ l) fun (i : Set (π' (f a))) ↦
    Sigma.map (β₁ := π) (β₂ := π') f g ⁻¹' Sigma.mk (β := π') (f a) '' id i

Tactic:
((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)

Premises used: Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, Sigma.map, Sigma.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
h :
  ∀ (x : Set (π' (f a))),
    Sigma.mk (β := π) a '' g a ⁻¹' id x = Sigma.map (β₁ := π) (β₂ := π') f g ⁻¹' Sigma.mk (β := π') (f a) '' id x
⊢ (comap (Sigma.map (β₁ := π) (β₂ := π') f g) (map (Sigma.mk (β := π') (f a)) l)).HasBasis
    (fun (s : Set (π' (f a))) ↦ s ∈ l) fun (i : Set (π' (f a))) ↦ Sigma.mk (β := π) a '' g a ⁻¹' id i

Tactic:
convert! ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)

Premises used: Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, Sigma.map, Sigma.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x : Set (π' (f a))
⊢ Sigma.mk (β := π) a '' g a ⁻¹' id x = Sigma.map (β₁ := π) (β₂ := π') f g ⁻¹' Sigma.mk (β := π') (f a) '' id x

Tactic:
apply image_sigmaMk_preimage_sigmaMap hf

Premises used: Set.image_sigmaMk_preimage_sigmaMap
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ (i : Set (Set α)), (i.Finite ∧ i ⊆ s) ∧ ⋂₀ i ⊆ U

Tactic:
simp only [mem_generate_iff, and_assoc, and_left_comm]

Premises used: and_left_comm, and_assoc, Filter.mem_generate_iff
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s_1 : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s a : Set (Set α)
fina : a.Finite
suba : a ⊆ s
b : Set (Set α)
finb : b.Finite
subb : b ⊆ s
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}) z ∧ z ⊆ ⋂₀ a ∩ ⋂₀ b

Tactic:
⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
        (sInter_union _ _).subset⟩

Premises used: Set.Finite.union, Set.sInter_union, Set.union_subset, Eq.subset, Set.mem_image_of_mem, And.intro, Exists.intro, Union.union, Set.sInter
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s_1 : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s a : Set (Set α)
fina : a.Finite
suba : a ⊆ s
b : Set (Set α)
finb : b.Finite
subb : b ⊆ s
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}) z ∧ z ⊆ ⋂₀ a ∩ ⋂₀ b

Tactic:
exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
        (sInter_union _ _).subset⟩
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
⊢ (ofSets s).sets = sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
rw :
  ⋯.filter (p := fun (t : Set (Set α)) ↦ t.Finite ∧ t ⊆ s) (s := fun (t : Set (Set α)) ↦ ⋂₀ t) =
    (FilterBasis.ofSets s).filter
⊢ generate s = generate (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s})

Tactic:
rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]

Premises used: Filter.hasBasis_generate, Filter.HasBasis.filter_eq, FilterBasis.generate, Filter.FilterBasis.ofSets_sets
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
⊢ ⋯.filter (p := fun (t : Set (Set α)) ↦ t.Finite ∧ t ⊆ s) (s := fun (t : Set (Set α)) ↦ ⋂₀ t) =
    (FilterBasis.ofSets s).filter

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
rw : generate (FilterBasis.ofSets s).sets = generate s
rw₁ : generate (sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}) = generate s
rw₂ rw₃ : generate s = generate s
⊢ (FilterBasis.ofSets s).filter = generate s

Tactic:
rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]

Premises used: Filter.FilterBasis.ofSets, Filter.generate_eq_generate_inter, FilterBasis.generate, Filter.FilterBasis.ofSets_sets
-- Module: Mathlib.Order.Filter.Bases.Finite
Goal:
α : Type u_1
s : Set (Set α)
⊢ (∀ {i : Set (Set α)}, i.Finite ∧ i ⊆ s → (⋂₀ i).Nonempty) ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty

Tactic:
simp only [← and_imp, and_comm]

Premises used: and_imp, and_comm
-- 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 α
mp :
  Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t →
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
mpr :
  (∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) →
    Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t ↔
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
constructor
-- 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 α
mp :
  (∃ (I : Set ι),
      I.Finite ∧
        ∃ (V : ι → Set α),
          (∀ (i : ι), ∃ (i_1 : ι' i), p i i_1 ∧ s i i_1 ⊆ V i) ∧
            (∀ i ∉ I, V i = univ) ∧ t = ⋂ i ∈ I, V i ∧ t = ⋂ (i : ι), V i) →
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) t →
    ∃ (i : Set ι × ((i : ι) → ι' i)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
simp only [mem_iInf', (hl _).mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.mem_iInf'
-- 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)
I : Set ι
hI : I.Finite
V : ι → Set α
hV : ∀ (i : ι), ∃ (i_1 : ι' i), p i i_1 ∧ s i i_1 ⊆ V i
mp :
  ∀ (u : (i : ι) → ι' i) (hu : ∀ (i : ι), p i (u i) ∧ s i (u i) ⊆ V i),
    ∃ (i : Set ι × ((i : ι) → ι' i)),
      (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
        Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)
⊢ ∃ (i : Set ι × ((i : ι) → ι' i)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
      Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)

Tactic:
choose u hu using hV
-- 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)
I : Set ι
hI : I.Finite
V : ι → Set α
u : (i : ι) → ι' i
hu : ∀ (i : ι), p i (u i) ∧ s i (u i) ⊆ V i
⊢ ∃ (i : Set ι × ((i : ι) → ι' i)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
      Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)

Tactic:
⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩

Premises used: Set.iInter₂_mono, Prod.mk, And.right, And.left, And.intro, Exists.intro
-- 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)
I : Set ι
hI : I.Finite
V : ι → Set α
u : (i : ι) → ι' i
hu : ∀ (i : ι), p i (u i) ∧ s i (u i) ⊆ V i
⊢ ∃ (i : Set ι × ((i : ι) → ι' i)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧
      Subset.{u_1} (α := Set α) (⋂ i_1 ∈ i.1, s i_1 (i.2 i_1)) (⋂ i ∈ I, V i)

Tactic:
exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩
-- 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
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
mpr : Membership.mem (γ := Filter α) (⨅ (i : ι), l i) (⋂ i ∈ (I, f).1, s i ((I, f).2 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
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) (⋂ i ∈ (I, f).1, s i ((I, f).2 i))

Tactic:
(biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.biInter_mem, Filter.HasBasis.mem_of_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
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), l i) (⋂ i ∈ (I, f).1, s i ((I, f).2 i))

Tactic:
exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Filter.biInter_mem, Filter.HasBasis.mem_of_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)
⊢ 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:
⟨fun t => ⟨fun ht => ?_, ?_⟩⟩

Premises used: Filter.HasBasis.mk, Iff.intro