awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
rw : {x : α | x ∈ s → Membership.mem (γ := Set α) ∅ x} ∈ f ↔ sᶜ ∈ f
⊢ f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f

Tactic:
rw [← empty_mem_iff_bot, mem_inf_principal]

Premises used: Filter.empty_mem_iff_bot, Filter.mem_inf_principal
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
⊢ {x : α | x ∈ s → Membership.mem (γ := Set α) ∅ x} ∈ f ↔ sᶜ ∈ f

Tactic:
simp only [mem_empty_iff_false, imp_false, compl_def]

Premises used: Set.compl_def, imp_false, Set.mem_empty_iff_false
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
h : f ⊓ 𝓟 sᶜ = ⊥
rwa : ∀ (h : sᶜᶜ ∈ f), s ∈ f
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : s ∈ f), s ∈ f
⊢ s ∈ f

Tactic:
rwa [inf_principal_eq_bot, compl_compl] at h

Premises used: compl_compl, Filter.inf_principal_eq_bot
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
hs : s ∈ f
t : Set α
⊢ s \ t ∈ f ⊓ 𝓟 tᶜ

Tactic:
inter_mem_inf hs <| mem_principal_self tᶜ

Premises used: Filter.mem_principal_self, Filter.inter_mem_inf, Set.Mem, Compl.compl, Set.diff, setOf, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f₁ f₂ : Filter (Filter α)
h : f₁ ≤ f₂
⊢ f₁.join ≤ f₂.join

Tactic:
fun _ hs => h hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P : α → Prop
⊢ (∀ᶠ (x : α) in f, P x) ↔ {x : α | P x} ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f₁ f₂ : Filter α
h : ∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x
⊢ f₁ = f₂

Tactic:
Filter.ext <| Set.setOf_bijective.surjective.forall.mpr h

Premises used: Iff.mpr, Function.Surjective.forall, Filter.ext, Function.Bijective.surjective, Set.setOf_bijective
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f₁ f₂ : Filter α
h : f₁ ≤ f₂
p : α → Prop
hp : ∀ᶠ (x : α) in f₂, p x
⊢ ∀ᶠ (x : α) in f₁, p x

Tactic:
h hp

Premises used: Filter.Eventually
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P : α → Prop
U : Set α
hU : U ∈ f
h : ∀ x ∈ U, P x
⊢ ∀ᶠ (x : α) in f, P x

Tactic:
mem_of_superset hU h

Premises used: Filter.Eventually, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
⊢ Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x

Tactic:
inter_mem

Premises used: Set.Mem, Filter.Eventually, Filter.inter_mem, setOf, Set.inter
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ ∀ᶠ (x : α) in f, True

Tactic:
univ_mem

Premises used: Set.Mem, Set.univ, Filter.Eventually, setOf, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∀ (x : α), p x
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
univ_mem' hp

Premises used: Filter.Eventually, Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ (∀ᶠ (x : α) in f, False) ↔ f = ⊥

Tactic:
empty_mem_iff_bot

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.empty_mem_iff_bot
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
pos : ∀ (h : p), (∀ᶠ (x : α) in f, p) ↔ p
neg : ∀ (h : ¬p), (∀ᶠ (x : α) in f, p) ↔ p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases h : p
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [h, t.ne]

Premises used: Filter.NeBot.ne
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [h, t.ne]

Premises used: Filter.NeBot.ne
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
⊢ (∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y

Tactic:
exists_mem_subset_iff.symm

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.exists_mem_subset_iff, Set.Subset, Iff.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
⊢ ∃ v ∈ f, ∀ y ∈ v, p y

Tactic:
eventually_iff_exists_mem.1 hp

Premises used: Iff.mp, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, p x → q x
⊢ ∀ᶠ (x : α) in f, q x

Tactic:
mp_mem hp hq

Premises used: Filter.Eventually, Filter.mp_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∀ (x : α), p x → q x
⊢ ∀ᶠ (x : α) in f, q x

Tactic:
hp.mp (Eventually.of_forall hq)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f : Filter α
p : α → β → Prop
h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y
⊢ ∀ (y : β), ∀ᶠ (x : α) in f, p x y

Tactic:
fun y => h.mono fun _ h => h y

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
⊢ (∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x

Tactic:
inter_mem_iff

Premises used: Set.Mem, Filter.Eventually, setOf, Set.inter, Filter.inter_mem_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p q : α → Prop
h' : ∀ᶠ (x : α) in f, p x
h : ∀ᶠ (x : α) in f, p x ↔ q x
⊢ ∀ᶠ (x : α) in f, q x

Tactic:
h'.mp (h.mono fun _ hx => hx.mp)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Iff.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x

Tactic:
simpa only [Iff.comm] using h

Premises used: Iff.comm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : Prop
q : α → Prop
h : p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : Prop
q : α → Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q

Tactic:
simp only [@or_comm _ q, eventually_or_distrib_left]

Premises used: Filter.eventually_or_distrib_left, or_comm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x

Tactic:
simp only [imp_iff_not_or, eventually_or_distrib_left]

Premises used: Filter.eventually_or_distrib_left, imp_iff_not_or
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
⊢ ∀ᶠ (x : α) in ⊥, p x

Tactic:
⟨⟩

Premises used: Set.Mem, Set.univ, Filter.Eventually, setOf, True.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
⊢ (∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f g : Filter α
⊢ (∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
fs : Set (Filter α)
⊢ (∀ᶠ (x : α) in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ (x : α) in f, p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
ι : Sort x
p : α → Prop
fs : ι → Filter α
⊢ (∀ᶠ (x : α) in ⨆ (b : ι), fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x

Tactic:
mem_iSup

Premises used: Filter.Eventually, Filter.mem_iSup
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
a : Set α
p : α → Prop
⊢ (∀ᶠ (x : α) in 𝓟 a, p x) ↔ ∀ x ∈ a, p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u_2
f : Filter α
s : Set α
P : α → Prop
hP : ∀ᶠ (x : α) in f, P x
hf : 𝓟 s ≤ f
⊢ ∀ x ∈ s, P x

Tactic:
Filter.eventually_principal.mp (hP.filter_mono hf)

Premises used: Filter.Eventually.filter_mono, Filter.eventually_principal, Iff.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f g : Filter α
p : α → Prop
⊢ (∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x

Tactic:
mem_inf_iff_superset

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Subset, Filter.mem_inf_iff_superset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
s : Set α
⊢ (∀ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x

Tactic:
mem_inf_principal

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.mem_inf_principal
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x : Set α
a : α
pa : p a
h₁ : a ∈ x → p a
⊢ a ∈ x → p a

Tactic:
_
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x : Set α
a : α
pa : p a
h_1 : a ∈ x
⊢ p a

Tactic:
pa
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x : Set α
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x_1 →
          Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ x_3 ∈ x → p x_3) x_2} x_1}
      a
h₂ h₃ : ∀ (a : α) (pa : p a), a ∈ x → p a
⊢ ∀ᶠ (x_1 : α) in f, x_1 ∈ x → p x_1

Tactic:
filter_upwards [h] with _ pa _ using pa
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
a : α
pa : Membership.mem (γ := Set α) univ a → p a
⊢ Membership.mem (γ := Set α) univ a

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → p x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x}
      a
h₂ h₃ : ∀ (a : α) (pa : Membership.mem (γ := Set α) univ a → p a), p a
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
filter_upwards [h univ] with _ pa using pa (by simp)

Premises used: Set.univ
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
⊢ ∃ᶠ (x : α) in f, p x

Tactic:
compl_notMem h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Filter.compl_notMem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : α → Prop
h : ∀ (x : α), p x
⊢ ∃ᶠ (x : α) in f, p x

Tactic:
Eventually.frequently (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
h : ∃ᶠ (x : α) in f, p x
hpq : ∀ᶠ (x : α) in f, p x → q x
⊢ ∃ᶠ (x : α) in f, q x

Tactic:
mt (fun hq => hq.mp <| hpq.mono fun _ => mt) h

Premises used: mt, Filter.Frequently, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
h : ∀ᶠ (x : α) in f, p x ↔ q x
⊢ (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x

Tactic:
⟨fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mp), fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mpr)⟩

Premises used: Iff.mpr, Filter.Eventually.mono, Iff.intro, Iff.mp, Filter.Frequently.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f g : Filter α
h : ∃ᶠ (x : α) in f, p x
hle : f ≤ g
⊢ ∃ᶠ (x : α) in g, p x

Tactic:
mt (fun h' => h'.filter_mono hle) h

Premises used: Filter.Eventually.filter_mono, mt, Filter.Frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
h : ∃ᶠ (x : α) in f, p x
hpq : ∀ (x : α), p x → q x
⊢ ∃ᶠ (x : α) in f, q x

Tactic:
h.mp (Eventually.of_forall hpq)

Premises used: Filter.Eventually.of_forall, Filter.Frequently.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
mt (fun h => hq.mp <| h.mono ?_) hp

Premises used: mt, Filter.Frequently, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
refine :
  ∀ (h : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ p x ∧ q x) x) (x : α),
    ¬(fun (x : α) ↦ p x ∧ q x) x → q x → ¬(fun (x : α) ↦ p x) x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
refine mt (fun h => hq.mp <| h.mono ?_) hp

Premises used: mt, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
h : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ p x ∧ q x) x
⊢ ∀ (x : α), ¬(fun (x : α) ↦ p x ∧ q x) x → q x → ¬(fun (x : α) ↦ p x) x

Tactic:
fun x hpq hq hp => hpq ⟨hp, hq⟩

Premises used: And.intro, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
h : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ p x ∧ q x) x
⊢ ∀ (x : α), ¬(fun (x : α) ↦ p x ∧ q x) x → q x → ¬(fun (x : α) ↦ p x) x

Tactic:
exact fun x hpq hq hp => hpq ⟨hp, hq⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
simpa only [and_comm] using hq.and_eventually hp

Premises used: and_comm, Filter.Frequently.and_eventually
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
by_contra : ∀ (H : ¬∃ (x : α), p x), False
⊢ ∃ (x : α), p x

Tactic:
by_contra H
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ (x : α), p x
⊢ ∀ᶠ (x : α) in f, ¬p x

Tactic:
replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False

Tactic:
hp H
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False

Tactic:
exact hp H
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
inst : f.NeBot
hp : ∀ᶠ (x : α) in f, p x
⊢ ∃ (x : α), p x

Tactic:
hp.frequently.exists

Premises used: Filter.Frequently.exists, Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
l : Filter α
p : α → Prop
rw : (∃ᶠ (x : α) in l, p x) ↔ {x : α | p x}ᶜ ∉ l
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x : α | p x}).NeBot

Tactic:
rw [neBot_iff, Ne, inf_principal_eq_bot]

Premises used: Filter.inf_principal_eq_bot, Filter.neBot_iff, Ne
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x : α | p x}ᶜ ∉ l

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
l : Filter α
s : Set α
⊢ (∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ 𝓟 s).NeBot

Tactic:
frequently_iff_neBot

Premises used: Set.Mem, setOf, Filter.frequently_iff_neBot
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ (x : α), p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ p x) x
⊢ False

Tactic:
simpa only [and_not_self_iff, exists_false] using H hp

Premises used: and_not_self_iff, exists_false
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _),
    Set.setOf_bijective.surjective.forall, Filter.Eventually, mem_setOf]

Premises used: Function.Surjective.forall, Filter.Eventually, and_comm, Set.mem_setOf, Function.Bijective.surjective, Set.setOf_bijective, Filter.frequently_iff_forall_eventually_exists_and
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
⊢ (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x

Tactic:
simp [Filter.Frequently]

Premises used: Filter.Frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f : Filter α
⊢ (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x

Tactic:
simp only [Filter.Frequently, not_not]

Premises used: Classical.not_not, Filter.Frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ f.NeBot

Tactic:
simp [frequently_iff_neBot]

Premises used: Filter.frequently_iff_neBot
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
⊢ ¬∃ᶠ (x : α) in f, False

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
pos : p → ((∃ᶠ (x : α) in f, p) ↔ p)
neg : ¬p → ((∃ᶠ (x : α) in f, p) ↔ p)
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases p
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
h : p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
h : ¬p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x

Tactic:
simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

Premises used: Filter.eventually_and, not_or, Filter.Frequently, not_and_or
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

Tactic:
simp [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x

Tactic:
simp [frequently_imp_distrib]

Premises used: Filter.frequently_imp_distrib
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

Tactic:
simp only [frequently_imp_distrib, frequently_const]

Premises used: Filter.frequently_const, Filter.frequently_imp_distrib
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

Tactic:
simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

Premises used: Filter.eventually_or_distrib_right, imp_iff_not_or, Filter.not_frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x

Tactic:
simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]

Premises used: Filter.Frequently, Classical.not_imp, Filter.eventually_imp_distrib_left, not_and
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

Tactic:
simp only [@and_comm _ q, frequently_and_distrib_left]

Premises used: Filter.frequently_and_distrib_left, and_comm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
⊢ ¬∃ᶠ (x : α) in ⊥, p x

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
⊢ (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ (x : α), p x

Tactic:
simp [Filter.Frequently]

Premises used: Filter.Frequently
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
a : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Tactic:
simp [Filter.Frequently, not_forall]

Premises used: Filter.Frequently, Classical.not_forall
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Tactic:
simp only [Filter.Frequently, eventually_inf_principal, not_and]

Premises used: Filter.eventually_inf_principal, Filter.Frequently, not_and
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
f g : Filter α
⊢ (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

Tactic:
simp only [Filter.Frequently, eventually_sup, not_and_or]

Premises used: Filter.Frequently, not_and_or, Filter.eventually_sup
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
p : α → Prop
fs : Set (Filter α)
⊢ (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x

Tactic:
simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]

Premises used: Filter.eventually_sSup, exists_prop, Filter.Frequently, Classical.not_forall
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ (b : β), fs b, p x) ↔ ∃ (b : β), ∃ᶠ (x : α) in fs b, p x

Tactic:
simp only [Filter.Frequently, eventually_iSup, not_forall]

Premises used: Filter.eventually_iSup, Filter.Frequently, Classical.not_forall
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
⊢ Nonempty β

Tactic:
haveI : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
this : Nonempty β
choose! :
  ∀ (f : (x : α) → β) (hf : ∀ (x : α) (hx : ∃ (y : β), r x y), r x (f x)), ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)
⊢ ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)

Tactic:
choose! f hf using fun x (hx : ∃ y, r x y) => hx
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
this : Nonempty β
f : (x : α) → β
hf : ∀ (x : α) (hx : ∃ (y : β), r x y), r x (f x)
⊢ ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)

Tactic:
⟨f, h.mono hf⟩

Premises used: Filter.Eventually.mono, Exists.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
this : Nonempty β
f : (x : α) → β
hf : ∀ (x : α) (hx : ∃ (y : β), r x y), r x (f x)
⊢ ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)

Tactic:
exact ⟨f, h.mono hf⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
ι : Type u_2
α : ι → Type u_3
inst : ∀ (i : ι), Nonempty.{u_3 + 1} (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩

Premises used: _private.0.Filter.skolem.match_1, Filter.Eventually, Exists, Filter.Eventually.of_forall, Filter.Eventually.mp, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
ι : Type u_2
α : ι → Type u_3
inst : ∀ (i : ι), Nonempty.{u_3 + 1} (α i)
P : (i : ι) → α i → Prop
F : Filter ι
refine : ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b), ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
⊢ (∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
-- Module: Mathlib.Order.Filter.Basic
Goal:
ι : Type u_2
α : ι → Type u_3
inst : ∀ (i : ι), Nonempty.{u_3 + 1} (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b
⊢ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩

Premises used: Exists, inferInstance, Nonempty.some, dite, Exists.intro, Exists.choose