awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
rcases :
  ∀ (W : Set α) (W_in : W ∈ B.sets) (W_sub : W ⊆ U ∩ V),
    ∃ (z : (↑B.sets : Type u_1)),
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
          ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
          ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
        (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
          ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
          ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)
⊢ ∃ (z : (↑B.sets : Type u_1)),
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)

Tactic:
rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩

Premises used: FilterBasis.inter_sets
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
h :
  (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in)) ∧
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in))
⊢ ∃ (z : (↑B.sets : Type u_1)),
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)

Tactic:
use ⟨W, W_in⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
h : W ⊆ U ∧ W ⊆ V
⊢ (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in)) ∧
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in))

Tactic:
simp only [le_principal_iff, mem_principal]

Premises used: Filter.le_principal_iff, Filter.mem_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V

Tactic:
subset_inter_iff.mp W_sub

Premises used: Set.subset_inter_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V

Tactic:
exact subset_inter_iff.mp W_sub

Premises used: Set.subset_inter_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
⊢ Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)

Tactic:
have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) := by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
this : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)
h : ∀ (U : Set α), U ∈ B.filter ↔ Membership.mem (γ := Filter α) (⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)) U
⊢ B.filter = ⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)

Tactic:
ext U
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
this : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)
U : Set α
⊢ U ∈ B.filter ↔ Membership.mem (γ := Filter α) (⨅ (s : (↑B.sets : Type u_1)), 𝓟 (↑s : Set α)) U

Tactic:
simp [mem_filter_iff, mem_iInf_of_directed this]

Premises used: FilterBasis.mem_filter_iff, Filter.mem_iInf_of_directed
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
a : generate B.sets ≤ B.filter
a₁ : B.filter ≤ generate B.sets
⊢ generate B.sets = B.filter

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
a : ∀ (V : Set α) (V_in : V ∈ B) (h : V ⊆ U), U ∈ generate B.sets
⊢ U ∈ generate B.sets

Tactic:
rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩

Premises used: FilterBasis.mem_filter_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets

Tactic:
GenerateSets.superset (GenerateSets.basic V_in) h

Premises used: Set.Mem, setOf, Filter.GenerateSets.superset, Filter.GenerateSets.basic
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets

Tactic:
exact GenerateSets.superset (GenerateSets.basic V_in) h

Premises used: Filter.GenerateSets.superset, Filter.GenerateSets.basic
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
a : B.sets ⊆ B.filter.sets
⊢ B.filter ≤ generate B.sets

Tactic:
rw [le_generate_iff]

Premises used: Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
⊢ B.sets ⊆ B.filter.sets

Tactic:
apply mem_filter_of_mem

Premises used: FilterBasis.mem_filter_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
F : FilterBasis α
⊢ F.filter.ker = ⋂₀ F.sets

Tactic:
aesop (add simp [ker, FilterBasis.filter])

Premises used: FilterBasis.filter, Filter.ker
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
U : Set α
⊢ U ∈ h.filter (p := p) (s := s) ↔ ∃ (i : ι), p i ∧ s i ⊆ U

Tactic:
simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff,
    exists_exists_and_eq_and]

Premises used: Filter.IsBasis.mem_filterBasis_iff, FilterBasis.mem_filter_iff, Filter.IsBasis.filter, exists_exists_and_eq_and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
rw : h.filterBasis (p := p) (s := s).filter = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
rw₁ : generate h.filterBasis (p := p) (s := s).sets = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
rw₂ rw₃ :
  generate { sets := {t : Set α | ∃ (i : ι), p i ∧ s i = t}, nonempty := ⋯, inter_sets := ⋯ : FilterBasis α }.sets =
    generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}
⊢ h.filter (p := p) (s := s) = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}

Tactic:
rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]

Premises used: Filter.IsBasis.filterBasis, Filter.IsBasis.filter, FilterBasis.generate
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
hl : l.HasBasis p s
⊢ t ∈ l ↔ ∃ (i : ι), p i ∧ s i ⊆ t

Tactic:
hl.mem_iff' t

Premises used: Filter.HasBasis.mem_iff'
-- 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
hl' : l'.HasBasis p s
h : ∀ (t : Set α), t ∈ l ↔ t ∈ l'
⊢ l = l'

Tactic:
ext t
-- 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
hl' : l'.HasBasis p s
t : Set α
h : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ t ∈ l'
h₁ h₂ : (∃ (i : ι), p i ∧ s i ⊆ t) ↔ ∃ (i : ι), p i ∧ s i ⊆ t
⊢ t ∈ l ↔ t ∈ l'

Tactic:
rw [hl.mem_iff, hl'.mem_iff]

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

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

Premises used: Filter.HasBasis.mk, Iff.intro, _private.0.Filter.hasBasis_iff.match_1
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ ∃ (i : ι), p i

Tactic:
(h.mem_iff.mp univ_mem).imp fun _ => And.left

Premises used: Filter.HasBasis.mem_iff, Exists.imp, And.left, Iff.mp, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ Nonempty ι

Tactic:
h.ex_mem.nonempty

Premises used: Exists.nonempty, Filter.HasBasis.ex_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
t : Set α
⊢ t ∈ h.filter (p := p) (s := s) ↔ ∃ (i : ι), p i ∧ s i ⊆ t

Tactic:
simp only [h.mem_filter_iff]

Premises used: Filter.IsBasis.mem_filter_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
hl : l.HasBasis p s
hi : p i
ht : s i ⊆ t
⊢ t ∈ l

Tactic:
hl.mem_iff.2 ⟨i, hi, ht⟩

Premises used: Iff.mpr, Filter.HasBasis.mem_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
i : ι
hl : l.HasBasis p s
hi : p i
⊢ s i ∈ l

Tactic:
hl.mem_of_superset hi Subset.rfl

Premises used: Filter.HasBasis.mem_of_superset, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
h : l.HasBasis p s
ht : t ∈ l
⊢ p (↑(h.index (p := p) (s := s) t ht) : ι)

Tactic:
(h.index t ht).2

Premises used: Filter.HasBasis.index, Subtype.property
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
h : l.HasBasis p s
ht : t ∈ l
⊢ s (↑(h.index (p := p) (s := s) t ht) : ι) ∈ l

Tactic:
h.mem_of_mem <| h.property_index _

Premises used: Filter.HasBasis.property_index, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
h : l.HasBasis p s
ht : t ∈ l
⊢ s (↑(h.index (p := p) (s := s) t ht) : ι) ⊆ t

Tactic:
(h.mem_iff.1 ht).choose_spec.2

Premises used: Exists.choose_spec, Filter.HasBasis.mem_iff, And.right, Iff.mp, Classical.choose
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
i j : ι
hi : p i
hj : p j
⊢ ∃ (k : ι), p k ∧ s k ⊆ s i ∩ s j

Tactic:
simpa only [h.mem_iff] using inter_mem (h.mem_of_mem hi) (h.mem_of_mem hj)

Premises used: Filter.HasBasis.mem_iff, Filter.inter_mem, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
h₁ : ∀ (U : Set α), U ∈ ⋯.filter (p := p) (s := s) ↔ U ∈ l
⊢ ⋯.filter (p := p) (s := s) = l

Tactic:
ext U
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
U : Set α
⊢ U ∈ ⋯.filter (p := p) (s := s) ↔ U ∈ l

Tactic:
simp [h.mem_iff, IsBasis.mem_filter_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.IsBasis.mem_filter_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
rw : l = ⋯.filter (p := p) (s := s)
rw₁ rw₂ : l = l
⊢ l = generate {U : Set α | ∃ (i : ι), p i ∧ s i = U}

Tactic:
rw [← h.isBasis.filter_eq_generate, h.filter_eq]

Premises used: Filter.IsBasis.filter_eq_generate, Filter.HasBasis.isBasis, Filter.HasBasis.filter_eq
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
⊢ B.filter.HasBasis (fun (s : Set α) ↦ s ∈ B) id

Tactic:
⟨fun _ => B.mem_filter_iff⟩

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

Tactic:
⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩

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

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
rcases : ∀ (i : ι) (hi : p i) (ht : s i ⊆ t), ∃ (i : ι'), p' i ∧ s' i ⊆ t
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t

Tactic:
rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht_1 : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
rcases : ∀ (i' : ι') (hi' : p' i') (hs's : s' i' ⊆ s i), ∃ (i : ι'), p' i ∧ s' i ⊆ t
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t

Tactic:
rcases h i hi with ⟨i', hi', hs's⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht_1 : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
i' : ι'
hi' : p' i'
hs's : s' i' ⊆ s i
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t

Tactic:
⟨i', hi', hs's.trans ht⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht_1 : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
i' : ι'
hi' : p' i'
hs's : s' i' ⊆ s i
⊢ ∃ (i : ι'), p' i ∧ s' i ⊆ t

Tactic:
exact ⟨i', hi', hs's.trans ht⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
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'
⊢ l.HasBasis p' s'

Tactic:
hl.to_hasBasis' h fun i' hi' =>
    let ⟨i, hi, hss'⟩ := h' i' hi'
    hl.mem_iff.2 ⟨i, hi, hss'⟩

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

Tactic:
simp only [hl.mem_iff, ← hp]

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

Tactic:
exists_congr fun i ↦
    and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, and_congr_right, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
p' : ι → Prop
s' : ι → Set α
hp : ∀ (i : ι), p i ↔ p' i
hs : ∀ (i : ι), p i → s i = s' i
t : Set α
⊢ (∃ (i : ι), p i ∧ s i ⊆ t) ↔ ∃ (i : ι), p i ∧ s' i ⊆ t

Tactic:
exact exists_congr fun i ↦
    and_congr_right fun hi ↦ hs i hi ▸ Iff.rfl

Premises used: and_congr_right, exists_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t : ι → Set α
h : ∀ (i : ι), p i → t i ⊆ s i
ht : ∀ (i : ι), p i → t i ∈ l
⊢ l.HasBasis p t

Tactic:
hl.to_hasBasis' (fun i hi => ⟨i, hi, h i hi⟩) ht

Premises used: And.intro, Exists.intro, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ᶠ (x : α) in l, q x) ↔ ∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x

Tactic:
simpa using hl.mem_iff

Premises used: Filter.HasBasis.mem_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
simp : (¬∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
simp only [Filter.Frequently, hl.eventually_iff]

Premises used: Filter.Frequently, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
push : (∀ (i : ι) (_ : p i), ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
⊢ (¬∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ (i : ι) (_ : p i), ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
P : Set α → Prop
mono : ∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s
⊢ (∃ s ∈ l, P s) ↔ ∃ (i : ι), p i ∧ P (s i)

Tactic:
⟨fun ⟨_s, hs, hP⟩ =>
    let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
    ⟨i, hi, mono his hP⟩,
    fun ⟨i, hi, hP⟩ => ⟨s i, hl.mem_of_mem hi, hP⟩⟩

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

Tactic:
⟨fun H i hi => H (s i) <| hl.mem_of_mem hi, fun H _s hs =>
    let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
    mono his (H i hi)⟩

Premises used: Filter.HasBasis.mem_iff, Iff.intro, Iff.mp, _private.0.Filter.HasBasis.to_hasBasis'.match_1, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ l.NeBot ↔ ∀ {i : ι}, p i → (s i).Nonempty

Tactic:
forall_mem_nonempty_iff_neBot.symm.trans <| hl.forall_iff fun _ _ => Nonempty.mono

Premises used: Filter.forall_mem_nonempty_iff_neBot, Set.Nonempty.mono, Iff.trans, Filter.HasBasis.forall_iff, Iff.symm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ (∀ {i : ι}, p i → (s i).Nonempty) ↔ ¬∃ (i : ι), p i ∧ s i = ∅

Tactic:
simp only [not_exists, not_and, nonempty_iff_ne_empty]

Premises used: not_exists, Set.nonempty_iff_ne_empty, not_and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
⊢ l.HasBasis (fun (s : Set α) ↦ s ∈ l) id

Tactic:
⟨fun _ => exists_mem_subset_iff.symm⟩

Premises used: Filter.exists_mem_subset_iff, Filter.HasBasis.mk, Iff.symm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
⊢ f.asBasis.filter = f

Tactic:
Filter.ext fun _ => exists_mem_subset_iff

Premises used: Filter.ext, Filter.exists_mem_subset_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
P : Set α → Prop
simp : (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
⊢ l.HasBasis (fun (s : Set α) ↦ s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
simp only [hasBasis_iff, id, and_assoc]

Premises used: id, Filter.hasBasis_iff, and_assoc
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
forall_congr' fun s =>
    ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

Premises used: Membership.mem, _private.0.Filter.hasBasis_self.match_2, Iff.intro, Iff.mp, forall_congr', Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
exact forall_congr' fun s =>
    ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
g : ι' → ι
hg : Function.Surjective g
⊢ l.HasBasis (p ∘ g) (s ∘ g)

Tactic:
⟨fun _ => h.mem_iff.trans hg.exists⟩

Premises used: Filter.HasBasis.mem_iff, Function.Surjective.exists, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
e : ι' ≃ ι
⊢ HasBasis.{u_1, u_5} (ι := ι') l (p ∘ (⇑e : (a : ι') → ι)) (s ∘ (⇑e : (a : ι') → ι))

Tactic:
h.comp_surjective e.surjective

Premises used: Equiv.surjective, Filter.HasBasis.comp_surjective
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : Set α
⊢ x ∈ l ↔ ∃ (i : Set α), (∃ (i_1 : ι), p i_1 ∧ s i_1 = i) ∧ id i ⊆ x

Tactic:
simp [h.mem_iff]

Premises used: Filter.HasBasis.mem_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
ι : Type u_6
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l.HasBasis (fun (x : Set α) ↦ x ∈ s '' {i : ι | p i}) id

Tactic:
h.to_image_id'

Premises used: Set.Mem, setOf, Filter.HasBasis.to_image_id', Set.image