awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
refine :
  Subset (α := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
      If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
⊢ Set.Countable.{u_6} (α := (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ))
    {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
      If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}

Tactic:
refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_

Premises used: id, Set.countable_range, SetLike.coe, Sigma.map, Set.Countable.mono
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f_1 : ι → Filter α
inst_1 : ∀ (i : ι), (f_1 i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f_1 i).HasAntitoneBasis (s i)
I : Set (PLift ι)
f : (i : (↑I : Type u_6)) → ℕ
hI :
  (Sigma.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)
      (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) I f)).Finite
⊢ I.Finite

Tactic:
hI
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f_1 : ι → Filter α
inst_1 : ∀ (i : ι), (f_1 i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f_1 i).HasAntitoneBasis (s i)
I : Set (PLift ι)
f : (i : (↑I : Type u_6)) → ℕ
hI :
  (Sigma.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)
      (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) I f)).Finite
lift :
  ∀ (I : Finset (PLift ι)) (f : (i : (↑(↑I : Set (PLift ι)) : Type u_6)) → ℕ),
    Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
      (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
        (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
          fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
      (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) (↑I : Set (PLift ι)) f)
⊢ Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
    (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) I f)

Tactic:
lift I to Finset (PLift ι) using hI

Premises used: Finset, PLift
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f_1 : ι → Filter α
inst_1 : ∀ (i : ι), (f_1 i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f_1 i).HasAntitoneBasis (s i)
I : Finset (PLift ι)
f : (i : (↑(↑I : Set (PLift ι)) : Type u_6)) → ℕ
⊢ Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
    (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) (↑I : Set (PLift ι)) f)

Tactic:
⟨⟨I, f⟩, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Sigma.mk, Set.range, rfl
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f_1 : ι → Filter α
inst_1 : ∀ (i : ι), (f_1 i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f_1 i).HasAntitoneBasis (s i)
I : Finset (PLift ι)
f : (i : (↑(↑I : Set (PLift ι)) : Type u_6)) → ℕ
⊢ Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
    (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) (↑I : Set (PLift ι)) f)

Tactic:
exact ⟨⟨I, f⟩, rfl⟩
-- Module: Mathlib.Order.Filter.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Type u_6
α : ι → Type u_7
inst : Countable ι
f : (i : ι) → Filter (α i)
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
⊢ (pi (α := α) f).IsCountablyGenerated

Tactic:
iInf.isCountablyGenerated _

Premises used: Filter.iInf.isCountablyGenerated, Filter.pi
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in l.curry m, p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, p (x, y)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
simp_rw : (¬∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ¬∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
simp_rw₁ : (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
simp_rw₂ : (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Tactic:
simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

Premises used: not_iff_not, Classical.not_not, Filter.Frequently, Filter.eventually_curry_iff
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set (α × β)
⊢ s ∈ l.curry m ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
⊢ l.curry m ≤ l ×ˢ m

Tactic:
fun _ => Eventually.curry

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.curry, Set.preimage
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h : ∀ᶠ (a : α) in la, Tendsto (fun (b : β) ↦ f a b) lb lc
⊢ Tendsto (↿f) (la.curry lb) lc

Tactic:
fun _s hs => h.mono fun _a ha => ha hs

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.mono, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
⊢ (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t

Tactic:
simp [frequently_curry_iff]

Premises used: Filter.frequently_curry_iff
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
inst : l.NeBot
inst_1 : m.NeBot
⊢ (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Tactic:
simp [eventually_curry_iff]

Premises used: Filter.eventually_curry_iff
-- Module: Mathlib.Order.Filter.Curry
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
hs : s ∈ l
ht : t ∈ m
⊢ s ×ˢ t ∈ l.curry m

Tactic:
curry_le_prod <| prod_mem_prod hs ht

Premises used: Filter.curry_le_prod, Filter.prod_mem_prod
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f g : Filter α
h : ∀ (s : Set α), s ∈ f ↔ s ∈ g
⊢ f = g

Tactic:
filter_eq <| Set.ext h

Premises used: Set.ext, Filter.filter_eq
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
t : Set (Set α)
h₁ : univ ∈ t
h₂ : ∀ {x y : Set α}, x ∈ t → x ⊆ y → y ∈ t
h₃ : ∀ {x y : Set α}, x ∈ t → y ∈ t → x ∩ y ∈ t
⊢ s ∈ { sets := t, univ_sets := h₁, sets_of_superset := @h₂, inter_sets := @h₃ : Filter α } ↔ s ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f.sets ↔ s ∈ f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
⊢ univ ∈ f

Tactic:
f.univ_sets

Premises used: Filter.univ_sets
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
x y : Set α
hx : x ∈ f
hxy : x ⊆ y
⊢ y ∈ f

Tactic:
f.sets_of_superset hx hxy

Premises used: Filter.sets_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
s : Set α
h : ∀ (a : α), a ∈ s
⊢ s ∈ f

Tactic:
mem_of_superset univ_mem fun x _ => h x

Premises used: Filter.univ_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ f
⊢ s ∩ t ∈ f

Tactic:
f.inter_sets hs ht

Premises used: Filter.inter_sets
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f
h : {x : α | x ∈ s → x ∈ t} ∈ f
⊢ t ∈ f

Tactic:
mem_of_superset (inter_mem hs h) fun _ ⟨h₁, h₂⟩ => h₂ h₁

Premises used: _private.0.Filter.mp_mem.match_1, Filter.inter_mem, Membership.mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
s : Set α
S : Set (Set α)
hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f
⊢ s ∈ f.copy S hmem ↔ s ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ (s : Set α), s ⊆ t → p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
⊢ Membership.mem (γ := Set (Set α)) {t : Set α | p tᶜ} univ

Tactic:
simpa
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ (s : Set α), s ⊆ t → p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
x y : Set α
ht₁ : Membership.mem (γ := Set (Set α)) {t : Set α | p tᶜ} x
ht₂ : Membership.mem (γ := Set (Set α)) {t : Set α | p tᶜ} y
⊢ Membership.mem (γ := Set (Set α)) {t : Set α | p tᶜ} (x ∩ y)

Tactic:
simp [compl_inter, hunion _ ht₁ _ ht₂]

Premises used: Set.compl_inter
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ (s : Set α), s ⊆ t → p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
s : Set α
⊢ s ∈ comk p he hmono hunion ↔ p sᶜ

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s t : Set α
⊢ s ∈ 𝓟 t ↔ t ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
α_1 : Type u_3
x : α_1
x_1 : Set α_1
⊢ Membership.mem (γ := Set (Set α_1)) {s : Set α_1 | x ∈ s} x_1 ↔ Membership.mem (γ := Filter α_1) (𝓟 {x}) x_1

Tactic:
simp
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
a : α
s : Set α
⊢ Membership.mem (γ := Filter α) (pure a) s ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g : Filter α
s t : Set α
f : Filter (Filter α)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | {t : Filter α | s ∈ t} ∈ f} univ

Tactic:
simp only [mem_setOf_eq, univ_mem, setOf_true]

Premises used: Set.mem_setOf_eq, Set.setOf_true, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
f : Filter (Filter α)
⊢ s ∈ f.join ↔ {t : Filter α | s ∈ t} ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f g : Filter α
⊢ f ≤ g ↔ ∀ (x : Set α), x ∈ g → x ∈ f

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
S : Set (Filter α)
⊢ s ∈ sSup S ↔ ∀ (f : Filter α), f ∈ S → s ∈ f

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set (Filter α)
⊢ sSup (lowerBounds s) = sInf s

Tactic:
simp [sInf, Filter.sInf]

Premises used: Filter.sInf, InfSet.sInf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∀ (x : α), x ∈ s} s ↔
      Membership.mem (γ := Filter α) (sSup (range pure)) s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
⊢ Membership.mem (γ := Filter α) ⊤ s ↔ ∀ (x : α), x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
rw : (∀ (x : α), x ∈ s) ↔ s = univ
rw₁ rw₂ : (∀ (x : α), x ∈ s) ↔ ∀ (x : α), x ∈ s
⊢ Membership.mem (γ := Filter α) ⊤ s ↔ s = univ

Tactic:
rw [mem_top_iff_forall, eq_univ_iff_forall]

Premises used: Filter.mem_top_iff_forall, Set.eq_univ_iff_forall
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
⊢ ∀ (s : Set α), Membership.mem (γ := Set (Set α)) univ s ↔ Membership.mem (γ := Filter α) (sSup ∅) s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
s : Set α
⊢ Membership.mem (γ := Filter α) ⊥ s

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
⊢ Eq.{u_1 + 1} (α := Set α) univ (univ ∩ univ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b} y

Tactic:
⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩

Premises used: Set.Mem, setOf, Set.subset_union_left, And.intro, Exists.intro, Union.union, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
refine : y = (a ∪ y) ∩ (b ∪ y)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b} y

Tactic:
refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
rw : y = a ∩ b ∪ y
rw₁ rw₂ : y = y
⊢ y = (a ∪ y) ∩ (b ∪ y)

Tactic:
rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]

Premises used: Set.inter_union_distrib_right, Set.union_eq_self_of_subset_left
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b}
    (a ∩ b ∩ (c ∩ d))

Tactic:
⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩

Premises used: Set.Mem, Filter.inter_mem, setOf, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
refine : a ∩ b ∩ (c ∩ d) = a ∩ c ∩ (b ∩ d)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b}
    (a ∩ b ∩ (c ∩ d))

Tactic:
refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ a ∩ b ∩ (c ∩ d) = a ∩ c ∩ (b ∩ d)

Tactic:
ac_rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
⊢ ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | s ∈ f ∧ s ∈ g} s ↔ Membership.mem (γ := Filter α) (sSup {f, g}) s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} univ

Tactic:
simp +contextual
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
rw : (x ∪ t) ∩ (y ∪ t) ∈ f
⊢ t ∈ f

Tactic:
rw [← union_eq_right.2 ht, inter_union_distrib_right]

Premises used: Iff.mpr, Set.inter_union_distrib_right, Set.union_eq_right
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
hs : x ∪ t ∈ f
ht₁ : y ∪ t ∈ f
⊢ (x ∪ t) ∩ (y ∪ t) ∈ f

Tactic:
apply inter_mem

Premises used: Filter.inter_mem
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ x ∪ t ∈ f

Tactic:
hx (mem_of_superset htg subset_union_right) subset_union_left

Premises used: Set.subset_union_right, Set.subset_union_left, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ x ∪ t ∈ f

Tactic:
exact hx (mem_of_superset htg subset_union_right) subset_union_left

Premises used: Set.subset_union_right, Set.subset_union_left, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ y ∪ t ∈ f

Tactic:
hy (mem_of_superset htg subset_union_right) subset_union_left

Premises used: Set.subset_union_right, Set.subset_union_left, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ y ∪ t ∈ f

Tactic:
exact hy (mem_of_superset htg subset_union_right) subset_union_left

Premises used: Set.subset_union_right, Set.subset_union_left, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f g : Filter α
s : Set α
⊢ s ∈ f \ g ↔ ∀ (t : Set α), t ∈ g → s ⊆ t → t ∈ f

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
⊢ ￢f = 𝓟 f.kerᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
f : Filter α
⊢ f.NeBot ↔ f ≠ ⊥

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

Premises used: Filter.NeBot.mk, Filter.NeBot.ne', Iff.intro
-- Module: Mathlib.Order.Filter.Defs
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = comap Prod.fst f ⊓ comap Prod.snd g

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
rwa : Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0
rwa₁ : Eq (α := ℝ) 0 0
rwa₂ : ¬BddBelow (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}
rwa₃ : Eq (α := ℝ) 0 0
rwa₄ rwa₅ rwa₆ : ¬BddBelow (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}
⊢ f.limsSup = 0

Tactic:
rwa [limsSup, sInf_of_not_bddBelow]

Premises used: Filter.limsSup, Real.sInf_of_not_bddBelow
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
⊢ Eq (α := ℝ) (sInf ∅) 0

Tactic:
sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
h : Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a} ∅
⊢ Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0

Tactic:
convert! sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
⊢ Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a} ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

Premises used: Filter.IsBounded, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0
rwa₁ : Eq (α := ℝ) 0 0
rwa₂ : ¬BddAbove (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}
rwa₃ : Eq (α := ℝ) 0 0
rwa₄ rwa₅ rwa₆ : ¬BddAbove (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}
⊢ f.limsInf = 0

Tactic:
rwa [limsInf, sSup_of_not_bddAbove]

Premises used: Filter.limsInf, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
⊢ Eq (α := ℝ) (sSup ∅) 0

Tactic:
sSup_empty

Premises used: Real.sSup_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
h : Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n} ∅
⊢ Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0

Tactic:
convert! sSup_empty

Premises used: Real.sSup_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
⊢ Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n} ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

Premises used: Filter.IsBounded, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ
hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
⊢ limsup u f = 0

Tactic:
limsSup_of_not_isCobounded hf

Premises used: Real.limsSup_of_not_isCobounded, Filter.limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ
hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
⊢ limsup u f = 0

Tactic:
limsSup_of_not_isBounded hf

Premises used: Filter.limsup, Real.limsSup_of_not_isBounded
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ
hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f u
⊢ liminf u f = 0

Tactic:
limsInf_of_not_isCobounded hf

Premises used: Filter.liminf, Real.limsInf_of_not_isCobounded