awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine :
  ∀ᶠ (i : ι) in F,
    P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯ : α i)) i)
⊢ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
-- 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
h : ∀ (i : ι) (hi : ∃ (b : α i), P i b), P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯)
⊢ ∀ᶠ (i : ι) in F,
    P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯ : α i)) i)

Tactic:
filter_upwards [H] with i hi
-- 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
i : ι
hi : ∃ (b : α i), P i b
⊢ P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯)

Tactic:
dif_pos hi ▸ hi.choose_spec

Premises used: Exists.choose_spec, Eq.rec, dif_pos, Eq.symm
-- 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
i : ι
hi : ∃ (b : α i), P i b
⊢ P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯)

Tactic:
exact dif_pos hi ▸ hi.choose_spec
-- 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)
refine₁ :
  ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b),
    ∀ᶠ (i : ι) in F,
      P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯ : α i)) i)
h :
  ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) (i : ι) (hi : ∃ (b : α i), P i b),
    P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯)
⊢ (∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
classical
  refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, f x = g x

Tactic:
h

Premises used: Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f g : α → β
⊢ f =ᶠ[⊤] g ↔ f = g

Tactic:
simp [EventuallyEq, funext_iff]

Premises used: funext_iff, Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
h : f =ᶠ[l] g
p : α → β → Prop
hf : ∀ᶠ (x : α) in l, p x (f x)
⊢ ∀ᶠ (x : α) in l, p x (g x)

Tactic:
hf.congr <| h.mono fun _ hx => hx ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, Filter.Eventually.mono, Filter.Eventually.congr
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t

Tactic:
eventually_congr <| Eventually.of_forall fun _ ↦ eq_iff_iff

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, Filter.eventually_congr, eq_iff_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
l : Filter α
⊢ s =ᶠ[l] univ ↔ s ∈ l

Tactic:
simp [eventuallyEq_set]

Premises used: Filter.eventuallyEq_set
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ ∃ s ∈ l, EqOn f g s

Tactic:
Eventually.exists_mem h

Premises used: Set.EqOn, Filter.Eventually.exists_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
s : Set α
hs : s ∈ l
h : EqOn f g s
⊢ f =ᶠ[l] g

Tactic:
eventually_of_mem hs h

Premises used: Filter.EventuallyEq, Filter.eventually_of_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ ∃ s ∈ l, EqOn f g s

Tactic:
eventually_iff_exists_mem

Premises used: Filter.EventuallyEq, Set.EqOn, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l l' : Filter α
f g : α → β
h₁ : f =ᶠ[l] g
h₂ : l' ≤ l
⊢ f =ᶠ[l'] g

Tactic:
h₂ h₁

Premises used: Filter.Eventually, Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f : α → β
⊢ f =ᶠ[l] f

Tactic:
Eventually.of_forall fun _ => rfl

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f : α → β
⊢ f =ᶠ[l] f

Tactic:
EventuallyEq.refl l f

Premises used: Filter.EventuallyEq.refl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
h : f = g
⊢ f =ᶠ[l] g

Tactic:
h ▸ .rfl

Premises used: Eq.rec, Filter.EventuallyEq.rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f g : α → β
l : Filter α
H : f =ᶠ[l] g
⊢ g =ᶠ[l] f

Tactic:
H.mono fun _ => Eq.symm

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, Eq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f g : α → β
l : Filter α
⊢ f =ᶠ[l] g ↔ g =ᶠ[l] f

Tactic:
⟨.symm, .symm⟩

Premises used: Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g h : α → β
H₁ : f =ᶠ[l] g
H₂ : g =ᶠ[l] h
⊢ f =ᶠ[l] h

Tactic:
H₂.rw (fun x y => f x = y) H₁

Premises used: Filter.EventuallyEq, Eq, Filter.EventuallyEq.rw
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g h : α → β
H : f =ᶠ[l] g
⊢ f =ᶠ[l] h ↔ g =ᶠ[l] h

Tactic:
⟨H.symm.trans, H.trans⟩

Premises used: Filter.EventuallyEq.trans, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g h : α → β
H : g =ᶠ[l] h
⊢ f =ᶠ[l] g ↔ f =ᶠ[l] h

Tactic:
⟨(·.trans H), (·.trans H.symm)⟩

Premises used: Filter.EventuallyEq.trans, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
x : α
h : g x = g' x
h_1 : f x = f' x
⊢ Eq (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f' x, g' x)) x)

Tactic:
simp only [*]
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f g : α → β
l : Filter α
H : f =ᶠ[l] g
h : β → γ
⊢ h ∘ f =ᶠ[l] h ∘ g

Tactic:
H.mono fun _ hx => congr_arg h hx

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, congr_arg
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
f f' : α → β
g g' : α → γ
l : Filter α
Hf : f =ᶠ[l] f'
h : β → γ → δ
Hg : g =ᶠ[l] g'
⊢ EventuallyEq.{u, u_2} (β := δ) l (fun (x : α) ↦ h (f x) (g x)) fun (x : α) ↦ h (f' x) (g' x)

Tactic:
(Hf.prodMk Hg).fun_comp (uncurry h)

Premises used: Function.uncurry, Filter.EventuallyEq.fun_comp, Filter.EventuallyEq.prodMk
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Mul β
f f' g g' : α → β
l : Filter α
h : f =ᶠ[l] g
h' : f' =ᶠ[l] g'
⊢ f * f' =ᶠ[l] g * g'

Tactic:
h.comp₂ (· * ·) h'

Premises used: HMul.hMul, Filter.EventuallyEq.comp₂
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
inst : Mul β
f₁ f₂ f₃ : α → β
h : f₁ =ᶠ[l] f₂
⊢ f₃ =ᶠ[l] f₃

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
γ : Type u_2
inst : Pow β γ
f g : α → β
l : Filter α
h : f =ᶠ[l] g
c : γ
⊢ f ^ c =ᶠ[l] g ^ c

Tactic:
h.fun_comp (· ^ c)

Premises used: HPow.hPow, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Inv β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f⁻¹ =ᶠ[l] g⁻¹

Tactic:
h.fun_comp Inv.inv

Premises used: Inv.inv, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Div β
f f' g g' : α → β
l : Filter α
h : f =ᶠ[l] g
h' : f' =ᶠ[l] g'
⊢ f / f' =ᶠ[l] g / g'

Tactic:
h.comp₂ (· / ·) h'

Premises used: HDiv.hDiv, Filter.EventuallyEq.comp₂
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
𝕜 : Type u_2
inst : SMul 𝕜 β
l : Filter α
f f' : α → 𝕜
g g' : α → β
hf : f =ᶠ[l] f'
hg : g =ᶠ[l] g'
⊢ EventuallyEq.{u, v} (β := β) l (fun (x : α) ↦ f x • g x) fun (x : α) ↦ f' x • g' x

Tactic:
hf.comp₂ (· • ·) hg

Premises used: Filter.EventuallyEq.comp₂, HSMul.hSMul
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
R : Type u_2
inst : Star R
f g : α → R
l : Filter α
h : f =ᶠ[l] g
⊢ star f =ᶠ[l] star g

Tactic:
h.fun_comp Star.star

Premises used: Filter.EventuallyEq.fun_comp, Star.star
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Max β
l : Filter α
f f' g g' : α → β
hf : f =ᶠ[l] f'
hg : g =ᶠ[l] g'
⊢ f ⊔ g =ᶠ[l] f' ⊔ g'

Tactic:
hf.comp₂ (· ⊔ ·) hg

Premises used: Filter.EventuallyEq.comp₂, Max.max
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Min β
l : Filter α
f f' g g' : α → β
hf : f =ᶠ[l] f'
hg : g =ᶠ[l] g'
⊢ f ⊓ g =ᶠ[l] f' ⊓ g'

Tactic:
hf.comp₂ (· ⊓ ·) hg

Premises used: Filter.EventuallyEq.comp₂, Min.min
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
l : Filter α
f g : α → β
h : f =ᶠ[l] g
s : Set β
⊢ f ⁻¹' s =ᶠ[l] g ⁻¹' s

Tactic:
h.fun_comp s

Premises used: Set.Mem, setOf, Set.preimage, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s =ᶠ[l] t
h' : s' =ᶠ[l] t'
⊢ s ∩ s' =ᶠ[l] t ∩ t'

Tactic:
h.comp₂ (· ∧ ·) h'

Premises used: Set.Mem, setOf, Filter.EventuallyEq.comp₂, Set.inter, And
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s =ᶠ[l] t
h' : s' =ᶠ[l] t'
⊢ s ∪ s' =ᶠ[l] t ∪ t'

Tactic:
h.comp₂ (· ∨ ·) h'

Premises used: Set.union, Set.Mem, setOf, Filter.EventuallyEq.comp₂, Or
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
h : s =ᶠ[l] t
⊢ sᶜ =ᶠ[l] tᶜ

Tactic:
h.fun_comp Not

Premises used: Set.Mem, setOf, Filter.EventuallyEq.fun_comp, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s =ᶠ[l] t
h' : s' =ᶠ[l] t'
⊢ s \ s' =ᶠ[l] t \ t'

Tactic:
h.inter h'.compl

Premises used: Set.Mem, Set.diff, setOf, Filter.EventuallyEq.inter, Filter.EventuallyEq.compl, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s =ᶠ[l] t
h' : s' =ᶠ[l] t'
⊢ s ∆ s' =ᶠ[l] t ∆ t'

Tactic:
(h.diff h').union (h'.diff h)

Premises used: Filter.EventuallyEq.diff, Filter.EventuallyEq.union, symmDiff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ s ↔ Membership.mem (γ := Set α) ∅ x) ↔ ∀ᶠ (x : α) in l, x ∉ s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t

Tactic:
simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]

Premises used: Set.mem_inter_iff, Filter.eventuallyEq_set, and_iff_left_iff_imp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
rw : t ∩ s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
rw₁ rw₂ : (∀ᶠ (x : α) in l, x ∈ t → x ∈ s) ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
rw [inter_comm, inter_eventuallyEq_left]

Premises used: Filter.inter_eventuallyEq_left, Set.inter_comm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
s : Set α
f g : α → β
⊢ f =ᶠ[𝓟 s] g ↔ EqOn f g s

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.EventuallyEq, Set.EqOn, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
F : Filter α
s : Set α
f g : α → β
⊢ f =ᶠ[F ⊓ 𝓟 s] g ↔ ∀ᶠ (x : α) in F, x ∈ s → f x = g x

Tactic:
eventually_inf_principal

Premises used: Filter.eventually_inf_principal, Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : AddGroup β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ f - g =ᶠ[l] 0

Tactic:
simpa using ((EventuallyEq.refl l f).sub h).symm

Premises used: Filter.EventuallyEq.refl, Filter.EventuallyEq.sub, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : AddGroup β
f g : α → β
l : Filter α
h : f - g =ᶠ[l] 0
⊢ f =ᶠ[l] g

Tactic:
simpa using h.add (EventuallyEq.refl l g)

Premises used: Filter.EventuallyEq.refl, Filter.EventuallyEq.add
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
f g : α → β
l : Filter α
⊢ f =ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x = g x

Tactic:
eventually_iff_all_subsets

Premises used: Filter.eventually_iff_all_subsets, Filter.EventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : LE β
l : Filter α
f f' g g' : α → β
H_1 : f ≤ᶠ[l] g
hf_1 : f =ᶠ[l] f'
hg_1 : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
rwa : ∀ (H : f' x ≤ g x), f' x ≤ g' x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : f' x ≤ g' x), f' x ≤ g' x
⊢ f' x ≤ g' x

Tactic:
rwa [hf, hg] at H
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : LE β
l : Filter α
f f' g g' : α → β
hf : f =ᶠ[l] f'
hg : g =ᶠ[l] g'
⊢ f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'

Tactic:
⟨fun H => H.congr hf hg, fun H => H.congr hf.symm hg.symm⟩

Premises used: Iff.intro, Filter.EventuallyLE.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : LE β
f g : α → β
l : Filter α
⊢ f ≤ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x ≤ g x

Tactic:
eventually_iff_all_subsets

Premises used: Filter.eventually_iff_all_subsets, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ f ≤ᶠ[l] g

Tactic:
h.mono fun _ => le_of_eq

Premises used: Filter.Eventually.mono, le_of_eq, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f : α → β
⊢ f ≤ᶠ[l] f

Tactic:
EventuallyEq.rfl.le

Premises used: Filter.EventuallyEq.le, Filter.EventuallyEq.rfl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f : α → β
⊢ f ≤ᶠ[l] f

Tactic:
EventuallyLE.refl l f

Premises used: Filter.EventuallyLE.refl
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f g h : α → β
H₁ : f ≤ᶠ[l] g
H₂ : g ≤ᶠ[l] h
⊢ f ≤ᶠ[l] h

Tactic:
H₂.mp <| H₁.mono fun _ => le_trans

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Filter.EventuallyLE, le_trans
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f g h : α → β
H₁ : f =ᶠ[l] g
H₂ : g ≤ᶠ[l] h
⊢ f ≤ᶠ[l] h

Tactic:
H₁.le.trans H₂

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.trans
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f g h : α → β
H₁ : f ≤ᶠ[l] g
H₂ : g =ᶠ[l] h
⊢ f ≤ᶠ[l] h

Tactic:
H₁.trans H₂.le

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.trans
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder β
l : Filter α
f g : α → β
h₁ : f ≤ᶠ[l] g
h₂ : g ≤ᶠ[l] f
⊢ f =ᶠ[l] g

Tactic:
h₂.mp <| h₁.mono fun _ => le_antisymm

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, le_antisymm, Filter.Eventually.mp
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder β
l : Filter α
f g : α → β
⊢ f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Tactic:
simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]

Premises used: Filter.eventually_and, Filter.EventuallyEq, le_antisymm_iff, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder β
l : Filter α
f g : α → β
h : f ≤ᶠ[l] g
⊢ g ≤ᶠ[l] f ↔ g =ᶠ[l] f

Tactic:
⟨fun h' => h'.antisymm h, EventuallyEq.le⟩

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Iff.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
f g : α → β
h : ∀ᶠ (x : α) in l, f x < g x
⊢ ∀ᶠ (x : α) in l, f x ≠ g x

Tactic:
h.mono fun _ hx => hx.ne

Premises used: Filter.Eventually.mono, LT.lt.ne
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
inst_1 : OrderTop β
l : Filter α
f g : α → β
h : ∀ᶠ (x : α) in l, f x < g x
⊢ ∀ᶠ (x : α) in l, f x ≠ ⊤

Tactic:
h.mono fun _ hx => hx.ne_top

Premises used: LT.lt.ne_top, Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder β
inst_1 : OrderTop β
l : Filter α
f : α → β
h : ∀ᶠ (x : α) in l, f x ≠ ⊤
⊢ ∀ᶠ (x : α) in l, f x < ⊤

Tactic:
h.mono fun _ hx => hx.lt_top

Premises used: Filter.Eventually.mono, Ne.lt_top
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : PartialOrder β
inst_1 : OrderTop β
l : Filter α
f : α → β
⊢ (∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤

Tactic:
⟨Eventually.ne_of_lt, Eventually.lt_top_of_ne⟩

Premises used: Filter.Eventually.lt_top_of_ne, Filter.Eventually.ne_of_lt, Iff.intro
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s ≤ᶠ[l] t
h' : s' ≤ᶠ[l] t'
⊢ s ∩ s' ≤ᶠ[l] t ∩ t'

Tactic:
h'.mp <| h.mono fun _ => And.imp

Premises used: And.imp, Filter.Eventually.mono, Filter.Eventually.mp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s ≤ᶠ[l] t
h' : s' ≤ᶠ[l] t'
⊢ s ∪ s' ≤ᶠ[l] t ∪ t'

Tactic:
h'.mp <| h.mono fun _ => Or.imp

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Or.imp, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
h : s ≤ᶠ[l] t
⊢ tᶜ ≤ᶠ[l] sᶜ

Tactic:
h.mono fun _ => mt

Premises used: mt, Filter.Eventually.mono, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t s' t' : Set α
l : Filter α
h : s ≤ᶠ[l] t
h' : t' ≤ᶠ[l] s'
⊢ s \ s' ≤ᶠ[l] t \ t'

Tactic:
h.inter h'.compl

Premises used: Set.Mem, Set.diff, setOf, Filter.EventuallyLE.inter, Filter.EventuallyLE.compl, Not
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ s ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s

Tactic:
eventually_inf_principal.symm

Premises used: Filter.eventually_inf_principal, Set.Mem, Filter.Eventually, setOf, Filter.EventuallyLE, Iff.symm
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ t ∈ l ⊓ 𝓟 s ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t

Tactic:
simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

Premises used: Filter.le_principal_iff, le_inf_iff, inf_le_left, true_and
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Tactic:
simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

Premises used: Filter.set_eventuallyLE_iff_inf_principal_le, Filter.eventuallyLE_antisymm_iff, le_antisymm_iff
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
x : α
hfx : f₁ x ≤ f₂ x
hgx : g₁ x ≤ g₂ x
⊢ (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x

Tactic:
sup_le_sup hfx hgx

Premises used: sup_le_sup
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α) (hfx : f₁ x ≤ f₂ x) (hgx : g₁ x ≤ g₂ x), (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Tactic:
filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
x : α
hfx : f x ≤ h x
hgx : g x ≤ h x
⊢ (f ⊔ g) x ≤ h x

Tactic:
_root_.sup_le hfx hgx

Premises used: sup_le
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ h x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ h x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f ⊔ g) x ≤ h x) x} x}
            x}
      a
h₂ h₃ : ∀ (x : α) (hfx : f x ≤ h x) (hgx : g x ≤ h x), (f ⊔ g) x ≤ h x
⊢ f ⊔ g ≤ᶠ[l] h

Tactic:
filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hf : h ≤ᶠ[l] f
⊢ h ≤ᶠ[l] f ⊔ g

Tactic:
hf.mono fun _ => _root_.le_sup_of_le_left

Premises used: le_sup_of_le_left, Filter.Eventually.mono, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hg : h ≤ᶠ[l] g
⊢ h ≤ᶠ[l] f ⊔ g

Tactic:
hg.mono fun _ => _root_.le_sup_of_le_right

Premises used: Filter.Eventually.mono, le_sup_of_le_right, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u
f : Filter (Filter α)
l : Filter α
h : ∀ᶠ (m : Filter α) in f, m ≤ l
⊢ f.join ≤ l

Tactic:
fun _ hs => h.mono fun _ hm => hm hs

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
h : EqOn f g s
⊢ f =ᶠ[𝓟 s] g

Tactic:
h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.EqOn, Set.Subset
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
l : Filter α
f g : α → β
h : EqOn f g s
hl : s ∈ l
⊢ f =ᶠ[l] g

Tactic:
h.eventuallyEq.filter_mono <| Filter.le_principal_iff.2 hl

Premises used: Iff.mpr, Filter.EventuallyEq.filter_mono, Filter.le_principal_iff, Set.EqOn.eventuallyEq
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u_1
l : Filter α
s t : Set α
h : s ⊆ t
⊢ s ≤ᶠ[l] t

Tactic:
Filter.Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Basic
Goal:
α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ 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:
simp
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
c : Cardinal.{u}
l : Filter α
S : Set (Set α)
inst : CardinalInterFilter l c
hSc : #(↑S : Type u) < c
⊢ ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l

Tactic:
⟨fun hS _s hs => mem_of_superset hS (sInter_subset_of_mem hs),
  CardinalInterFilter.cardinal_sInter_mem _ hSc⟩

Premises used: Set.sInter_subset_of_mem, Iff.intro, CardinalInterFilter.cardinal_sInter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
α : Type u
l : Filter α
⊢ ∀ (S : Set (Set α)), #(↑S : Type u) < ℵ₀ → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l

Tactic:
simp_all only [lt_aleph0_iff_subtype_finite, setOf_mem_eq, sInter_mem,
      implies_true]

Premises used: Set.setOf_mem_eq, Cardinal.lt_aleph0_iff_subtype_finite, Filter.sInter_mem, implies_true
-- Module: Mathlib.Order.Filter.CardinalInter
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 l : Filter α
inst : CountableInterFilter l
S : Set (Set α)
hS : #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
a : ∀ s ∈ S, s ∈ l
apply : S.Countable
⊢ ⋂₀ S ∈ l

Tactic:
apply CountableInterFilter.countable_sInter_mem S _ a

Premises used: CountableInterFilter.countable_sInter_mem