awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s ↔ s ∈ f

Tactic:
⟨fun h => h Subset.rfl, fun hs _ ht => mem_of_superset hs ht⟩

Premises used: Set.Subset.rfl, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ Iic (𝓟 s) = {l : Filter α | s ∈ l}

Tactic:
Set.ext fun _ => le_principal_iff

Premises used: Set.ext, Filter.le_principal_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
⊢ 𝓟 s ≤ 𝓟 t ↔ s ⊆ t

Tactic:
simp only [le_principal_iff, mem_principal]

Premises used: Filter.le_principal_iff, Filter.mem_principal
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Monotone.{u, u} (α := Set α) 𝓟

Tactic:
fun _ _ => principal_mono.2

Premises used: Iff.mpr, Filter.principal_mono, Monotone
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
simp : s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
⊢ 𝓟 s = 𝓟 t ↔ s = t

Tactic:
simp only [le_antisymm_iff, le_principal_iff, mem_principal]

Premises used: Filter.le_principal_iff, Filter.mem_principal, le_antisymm_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Filter α)
⊢ (𝓟 s).join = sSup s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ LE.le.{u} (α := Filter α) ⊤ (𝓟 univ)

Tactic:
simp only [le_principal_iff, mem_top]

Premises used: Filter.le_principal_iff, Filter.mem_top
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Filter α) (𝓟 ∅) ⊥

Tactic:
bot_unique fun _ _ => empty_subset _

Premises used: Set.empty_subset, bot_unique
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
S : Set (Set α)
f : Filter α
⊢ f ≤ generate S ↔ f ≤ ⨅ s ∈ S, 𝓟 s

Tactic:
simp [le_generate_iff, le_principal_iff, subset_def]

Premises used: Filter.le_principal_iff, Set.subset_def, Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ ∅ ∈ f ↔ f = ⊥

Tactic:
⟨fun h => bot_unique fun s _ => mem_of_superset h (empty_subset s), fun h => h.symm ▸ mem_bot⟩

Premises used: Filter.mem_bot, Eq.rec, Iff.intro, Set.empty_subset, bot_unique, Eq.symm, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
hf : f.NeBot
s : Set α
hs : s ∈ f
⊢ s.Nonempty

Tactic:
s.eq_empty_or_nonempty.elim (fun h => absurd hs (h.symm ▸ mt empty_mem_iff_bot.mp hf.1)) id

Premises used: mt, Eq.rec, id, Set.eq_empty_or_nonempty, absurd, Filter.NeBot.ne', Filter.empty_mem_iff_bot, Iff.mp, Or.elim, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
hf : f.NeBot
s : Set α
hs : s ∈ f
⊢ s.Nonempty

Tactic:
@Filter.nonempty_of_mem α f hf s hs

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
⊢ ∅ ∉ f

Tactic:
fun h => (nonempty_of_mem h).ne_empty rfl

Premises used: Set.Nonempty.ne_empty, Filter.nonempty_of_mem, Not, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
⊢ Nonempty α

Tactic:
Exists.nonempty <| nonempty_of_mem (univ_mem : univ ∈ f)

Premises used: Exists.nonempty, Filter.nonempty_of_mem, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
inst : f.NeBot
h : s ∈ f
⊢ sᶜ ∉ f

Tactic:
fun hsc =>
  (nonempty_of_mem (inter_mem h hsc)).ne_empty <| inter_compl_self s

Premises used: Set.Nonempty.ne_empty, Filter.inter_mem, Filter.nonempty_of_mem, Set.inter_compl_self, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : IsEmpty α
f : Filter α
⊢ f = ⊥

Tactic:
empty_mem_iff_bot.mp <| univ_mem' isEmptyElim

Premises used: isEmptyElim, Filter.empty_mem_iff_bot, Iff.mp, Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

Tactic:
simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff, inf_eq_inter, bot_eq_empty,
    @eq_comm _ ∅]

Premises used: disjoint_iff, Set.bot_eq_empty, eq_comm, Filter.empty_mem_iff_bot, Filter.mem_inf_iff, Set.inf_eq_inter
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
s t : Set α
h : Disjoint s t
hs : s ∈ f
ht : t ∈ g
⊢ Disjoint f g

Tactic:
Filter.disjoint_iff.mpr ⟨s, hs, t, ht, h⟩

Premises used: Iff.mpr, Filter.disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
hf : f.NeBot
hs : s ∈ f
ht : t ∈ f
⊢ ¬Disjoint s t

Tactic:
fun h =>
  not_disjoint_self_iff.2 hf <| Filter.disjoint_iff.2 ⟨s, hs, t, ht, h⟩

Premises used: Iff.mpr, Filter.disjoint_iff, Filter.not_disjoint_self_iff, And.intro, Exists.intro, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
⊢ f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Tactic:
simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

Premises used: Filter.disjoint_iff, disjoint_iff, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
hf : f.NeBot
⊢ Nonempty α

Tactic:
not_isEmpty_iff.mp fun _ ↦ hf.ne (Subsingleton.elim _ _)

Premises used: Filter.NeBot.ne, Bot.bot, not_isEmpty_iff, Iff.mp, Subsingleton.elim
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
⊢ l = ⊤

Tactic:
top_unique fun s hs => ?_

Premises used: top_unique
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
refine : ∀ (s : Set α) (hs : s ∈ l), Membership.mem (γ := Filter α) ⊤ s
⊢ l = ⊤

Tactic:
refine top_unique fun s hs => ?_

Premises used: top_unique
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
s : Set α
hs : s ∈ l
⊢ s = univ

Tactic:
Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)

Premises used: Filter.nonempty_of_mem, Subsingleton.eq_univ_of_nonempty
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
s : Set α
hs : s ∈ l
obtain : ∀ (hs : univ ∈ l), Membership.mem (γ := Filter α) ⊤ univ
⊢ Membership.mem (γ := Filter α) ⊤ s

Tactic:
obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)

Premises used: Set.univ, Filter.nonempty_of_mem, Subsingleton.eq_univ_of_nonempty, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
hs : univ ∈ l
⊢ Membership.mem (γ := Filter α) ⊤ univ

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
hs : univ ∈ l
⊢ Membership.mem (γ := Filter α) ⊤ univ

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ (∀ s ∈ f, s.Nonempty) ↔ f.NeBot

Tactic:
⟨fun h => ⟨fun hf => not_nonempty_empty (h ∅ <| hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩

Premises used: Set.not_nonempty_empty, Filter.mem_bot, Eq.rec, Filter.NeBot.mk, Filter.nonempty_of_mem, Iff.intro, EmptyCollection.emptyCollection, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s_1 t : Set α
inst : Nonempty α
s : Set α
hs : Membership.mem (γ := Filter α) ⊤ s
rwa : Set.Nonempty.{u} (α := α) univ
rwa₁ rwa₂ rwa₃ rwa₄ : Nonempty α
⊢ s.Nonempty

Tactic:
rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]

Premises used: Set.nonempty_iff_univ_nonempty, Iff.mp, Filter.mem_top
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s t : Set α
inst : Nonempty α
⊢ Nontrivial.{u} (Filter α)

Tactic:
⟨⟨⊤, ⊥, instNeBotTop.ne⟩⟩

Premises used: Filter.NeBot.ne, Filter.instNeBotTop, Bot.bot, Nontrivial.mk, Exists.intro, Top.top
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
⊢ Nontrivial.{u} (Filter α) ↔ Nonempty α

Tactic:
⟨fun _ =>
    by_contra fun h' =>
      haveI := not_nonempty_iff.1 h'
      not_subsingleton (Filter α) inferInstance,
    @Filter.instNontrivialFilter α⟩

Premises used: Filter.instNontrivialFilter, inferInstance, Iff.intro, not_subsingleton, by_contra, Filter
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
S : Set (Filter α)
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ f ∈ S, s ∈ f
⊢ l = sInf S

Tactic:
le_antisymm (le_sInf fun f hf _ hs => h.2 ⟨f, hf, hs⟩)
    fun _ hs => let ⟨_, hf, hs⟩ := h.1 hs; (sInf_le hf) hs

Premises used: Iff.mpr, Membership.mem, le_antisymm, sInf_le, And.intro, Exists.intro, Iff.mp, le_sInf, InfSet.sInf, _private.0.Filter.eq_sInf_of_mem_iff_exists_mem.match_1
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), s ∈ f i
⊢ l = iInf f

Tactic:
eq_sInf_of_mem_iff_exists_mem <| h.trans (exists_range_iff (p := (_ ∈ ·))).symm

Premises used: iInf, Set.exists_range_iff, Iff.trans, Filter.eq_sInf_of_mem_iff_exists_mem, Iff.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i
rw : l = ⨅ (x : Subtype p), f (↑x : ι)
⊢ l = ⨅ (i : ι), ⨅ (_ : p i), f i

Tactic:
rw [iInf_subtype']

Premises used: iInf_subtype'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i
x : Set α
⊢ x ∈ l ↔ ∃ (i : Subtype p), x ∈ f (↑i : ι)

Tactic:
simp only [Subtype.exists, h, exists_prop]

Premises used: Subtype.exists, exists_prop
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i
⊢ l = ⨅ (x : Subtype p), f (↑x : ι)

Tactic:
exact eq_iInf_of_mem_iff_exists_mem fun {_} => by simp only [Subtype.exists, h, exists_prop]

Premises used: Filter.eq_iInf_of_mem_iff_exists_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
simp : ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ (i : ι), y ∈ (f i).sets
⊢ ∀ {x y : Set α},
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) x →
      x ⊆ y → Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) y

Tactic:
simp only [mem_iUnion, exists_imp]

Premises used: Set.mem_iUnion, exists_imp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
⊢ ∀ (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ (i : ι), y ∈ (f i).sets

Tactic:
fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩

Premises used: Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ (i : ι), y ∈ (f i).sets

Tactic:
exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
simp : ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ (i : ι), x ∩ y ∈ (f i).sets
⊢ ∀ {x y : Set α},
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) x →
      Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) y →
        Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) (x ∩ y)

Tactic:
simp only [mem_iUnion, exists_imp]

Premises used: Set.mem_iUnion, exists_imp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
rcases : ∀ (c : ι) (ha : f a ≥ f c) (hb : f b ≥ f c), ∃ (i : ι), x ∩ y ∈ (f i).sets
⊢ ∃ (i : ι), x ∩ y ∈ (f i).sets

Tactic:
rcases h a b with ⟨c, ha, hb⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ (i : ι), x ∩ y ∈ (f i).sets

Tactic:
⟨c, inter_mem (ha hx) (hb hy)⟩

Premises used: Filter.inter_mem, Exists.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ (i : ι), x ∩ y ∈ (f i).sets

Tactic:
exact ⟨c, inter_mem (ha hx) (hb hy)⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
inst : Nonempty ι
s : Set α
⊢ s ∈ iInf f ↔ ∃ (i : ι), s ∈ f i

Tactic:
simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]

Premises used: Filter.iInf_sets_eq, Filter.mem_sets, Set.mem_iUnion
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ Nonempty.{v + 1} (↑s : Type v)

Tactic:
haveI := ne.to_subtype
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty.{v + 1} (↑s : Type v)
simp_rw : Membership.mem (γ := Filter α) (⨅ (x : Subtype (Membership.mem s)), f (↑x : β)) t ↔ ∃ i ∈ s, t ∈ f i
simp_rw₁ : (∃ (i : { x : β // x ∈ s }), t ∈ f (↑i : β)) ↔ ∃ i ∈ s, t ∈ f i
simp_rw₂ : (∃ (a : β) (_ : a ∈ s), t ∈ f a) ↔ ∃ i ∈ s, t ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ s, f i) t ↔ ∃ i ∈ s, t ∈ f i

Tactic:
simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

Premises used: Subtype.exists, iInf_subtype', exists_prop, DirectedOn.directed_val, Filter.mem_iInf_of_directed
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ Membership.mem (γ := Set (Set α)) (sets (⨅ i ∈ s, f i)) t ↔ Membership.mem (γ := Set (Set α)) (⋃ i ∈ s, (f i).sets) t

Tactic:
simp [mem_biInf_of_directed h ne]

Premises used: Filter.mem_biInf_of_directed
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f₁ f₂ : Filter (Filter α)
x : Set α
⊢ x ∈ f₁.join ⊔ f₂.join ↔ x ∈ (f₁ ⊔ f₂).join

Tactic:
simp only [mem_sup, mem_join]

Premises used: Filter.mem_sup, Filter.mem_join
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort w
f : ι → Filter (Filter α)
x : Set α
⊢ Membership.mem (γ := Filter α) (⨆ (x : ι), (f x).join) x ↔ Membership.mem (γ := Filter α) (join (⨆ (x : ι), f x)) x

Tactic:
simp only [mem_iSup, mem_join]

Premises used: Filter.mem_iSup, Filter.mem_join
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f_1 g : Filter α
s t : Set α
f : Filter α
h : ∀ (s : Set α), s ∈ ⊤ \ f ↔ s ∈ ￢f
⊢ ⊤ \ f = ￢f

Tactic:
ext s
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f_1 g : Filter α
s_1 t : Set α
f : Filter α
s : Set α
h : (∀ t ∈ f, ∀ (x : α), x ∈ s ∨ x ∈ t) ↔ ∀ (x : α), (∀ t ∈ f, x ∈ t) ∨ x ∈ s
⊢ s ∈ ⊤ \ f ↔ s ∈ ￢f

Tactic:
simp only [mem_sdiff_iff_union, Filter.hnot_def, mem_principal, compl_subset_iff_union,
      mem_top_iff_forall, eq_univ_iff_forall, ker, mem_union, mem_sInter, Filter.mem_sets]

Premises used: Set.mem_union, Filter.mem_top_iff_forall, Filter.mem_sets, Set.eq_univ_iff_forall, Filter.mem_principal, Set.compl_subset_iff_union, Filter.hnot_def, Set.mem_sInter, Filter.mem_sdiff_iff_union, Filter.ker
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f_1 g : Filter α
s_1 t : Set α
f : Filter α
s : Set α
⊢ (∀ t ∈ f, ∀ (x : α), x ∈ s ∨ x ∈ t) ↔ ∀ (x : α), (∀ t ∈ f, x ∈ t) ∨ x ∈ s

Tactic:
grind
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
inst : Nonempty ι
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
⊢ ¬(iInf f).NeBot → ¬∀ (i : ι), (f i).NeBot

Tactic:
simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
    mem_iInf_of_directed hd] using id

Premises used: id, Filter.empty_mem_iff_bot, Filter.not_neBot, Filter.mem_iInf_of_directed, Classical.not_forall
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
inl : IsEmpty ι → (iInf f).NeBot
inr : Nonempty ι → (iInf f).NeBot
⊢ (iInf f).NeBot

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h : IsEmpty ι
inl : iInf f ≠ ⊥
⊢ (iInf f).NeBot

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h : IsEmpty ι
⊢ iInf f ≠ ⊥

Tactic:
simp [iInf_of_empty f, top_ne_bot]

Premises used: iInf_of_empty, top_ne_bot
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h : Nonempty ι
⊢ (iInf f).NeBot

Tactic:
iInf_neBot_of_directed' hd hb

Premises used: Filter.iInf_neBot_of_directed'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h : Nonempty ι
⊢ (iInf f).NeBot

Tactic:
exact iInf_neBot_of_directed' hd hb

Premises used: Filter.iInf_neBot_of_directed'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set (Filter α)
hne : s.Nonempty
hd : DirectedOn (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
hbot : ⊥ ∉ s
⊢ (sInf s).NeBot

Tactic:
(sInf_eq_iInf' s).symm ▸
    @iInf_neBot_of_directed' _ _ _ hne.to_subtype hd.directed_val fun ⟨_, hf⟩ =>
      ⟨ne_of_mem_of_not_mem hf hbot⟩

Premises used: Filter.NeBot, Eq.rec, Filter.NeBot.mk, DirectedOn.directed_val, ne_of_mem_of_not_mem, sInf_eq_iInf', Eq.symm, Subtype.val, Filter.iInf_neBot_of_directed', _private.0.Filter.sInf_neBot_of_directed'.match_1
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
inst : Nonempty α
s : Set (Filter α)
hd : DirectedOn (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
hbot : ⊥ ∉ s
⊢ (sInf s).NeBot

Tactic:
(sInf_eq_iInf' s).symm ▸
    iInf_neBot_of_directed hd.directed_val fun ⟨_, hf⟩ => ⟨ne_of_mem_of_not_mem hf hbot⟩

Premises used: Filter.NeBot, Eq.rec, Filter.NeBot.mk, DirectedOn.directed_val, ne_of_mem_of_not_mem, sInf_eq_iInf', Filter.iInf_neBot_of_directed, Eq.symm, Subtype.val, _private.0.Filter.sInf_neBot_of_directed'.match_1
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
inst : Nonempty ι
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
⊢ (iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot

Tactic:
⟨fun H i => H.mono (iInf_le _ i), iInf_neBot_of_directed' hd⟩

Premises used: Filter.NeBot.mono, Iff.intro, iInf_le, Filter.iInf_neBot_of_directed'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
inst : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
⊢ (iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot

Tactic:
⟨fun H i => H.mono (iInf_le _ i), iInf_neBot_of_directed hd⟩

Premises used: Filter.NeBot.mono, Filter.iInf_neBot_of_directed, Iff.intro, iInf_le
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
simp : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)

Tactic:
simp only [le_principal_iff, mem_inf_iff]

Premises used: Filter.le_principal_iff, Filter.mem_inf_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Tactic:
⟨s, Subset.rfl, t, Subset.rfl, rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Tactic:
exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
⊢ 𝓟 (s ∩ t) ≤ 𝓟 s ⊓ 𝓟 t

Tactic:
simp [le_inf_iff, inter_subset_left, inter_subset_right]

Premises used: Set.inter_subset_left, le_inf_iff, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t u : Set α
⊢ u ∈ 𝓟 s ⊔ 𝓟 t ↔ u ∈ 𝓟 (s ∪ t)

Tactic:
simp only [union_subset_iff, mem_sup, mem_principal]

Premises used: Set.union_subset_iff, Filter.mem_principal, Filter.mem_sup
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort w
s : ι → Set α
x : Set α
⊢ Membership.mem (γ := Filter α) (⨆ (x : ι), 𝓟 (s x)) x ↔ Membership.mem (γ := Filter α) (𝓟 (⋃ (i : ι), s i)) x

Tactic:
simp only [mem_iSup, mem_principal, iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Filter.mem_iSup, Filter.mem_principal
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t x : Set α
⊢ x ∈ 𝓟 s \ 𝓟 t ↔ x ∈ 𝓟 (s \ t)

Tactic:
simp [← le_principal_iff, principal_mono]

Premises used: Filter.le_principal_iff, Filter.principal_mono
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ ￢𝓟 s = 𝓟 sᶜ

Tactic:
simpa [← compl_eq_univ_diff] using @principal_sdiff_principal _ univ s

Premises used: Filter.principal_sdiff_principal, Set.compl_eq_univ_diff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ 𝓟 s = ⊥ ↔ s = ∅

Tactic:
empty_mem_iff_bot.symm.trans <| mem_principal.trans subset_empty_iff

Premises used: Filter.mem_principal, Filter.empty_mem_iff_bot, Iff.trans, Set.subset_empty_iff, Iff.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
⊢ (𝓟 s).NeBot ↔ s.Nonempty

Tactic:
neBot_iff.trans <| (not_congr principal_eq_bot_iff).trans nonempty_iff_ne_empty.symm

Premises used: Filter.neBot_iff, Filter.principal_eq_bot_iff, Set.nonempty_iff_ne_empty, Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∩ sᶜ) = ⊥
rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 ∅) ⊥
rw₂ rw₃ : Eq.{u + 1} (α := Filter α) ⊥ ⊥
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥

Tactic:
rw [inf_principal, inter_compl_self, principal_empty]

Premises used: Filter.inf_principal, Filter.principal_empty, Set.inter_compl_self
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∪ sᶜ) = ⊤
rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 univ) ⊤
rw₂ rw₃ : Eq.{u + 1} (α := Filter α) ⊤ ⊤
⊢ 𝓟 s ⊔ 𝓟 sᶜ = ⊤

Tactic:
rw [sup_principal, union_compl_self, principal_univ]

Premises used: Filter.sup_principal, Filter.principal_univ, Set.union_compl_self
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f

Tactic:
simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
    ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

Premises used: Filter.le_principal_iff, compl_compl, Filter.inf_principal, Compl.compl, Set.compl_inter, disjoint_assoc, Inter.inter, IsCompl.le_left_iff, Filter.isCompl_principal, IsCompl.le_right_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ {x : α | x ∈ t → x ∈ s} ∈ f

Tactic:
simp only [mem_inf_principal', imp_iff_not_or, setOf_or, compl_def, setOf_mem_eq]

Premises used: Set.compl_def, imp_iff_not_or, Set.setOf_mem_eq, Set.setOf_or, Filter.mem_inf_principal'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
h : ∀ (s_1 : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i ⊓ 𝓟 s) s_1 ↔ s_1 ∈ (⨆ (i : ι), f i) ⊓ 𝓟 s
⊢ ⨆ (i : ι), f i ⊓ 𝓟 s = (⨆ (i : ι), f i) ⊓ 𝓟 s

Tactic:
ext
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s s_1 : Set α
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), f i ⊓ 𝓟 s) s_1 ↔ s_1 ∈ (⨆ (i : ι), f i) ⊓ 𝓟 s

Tactic:
simp only [mem_iSup, mem_inf_principal]

Premises used: Filter.mem_iSup, Filter.mem_inf_principal