awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
a₀ : α
others_bigger : ∀ b ∈ {y : α | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a

Tactic:
fun h => others_bigger a ⟨h, has⟩

Premises used: And.intro
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
a₀ : α
others_bigger : ∀ b ∈ {y : α | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a

Tactic:
exact fun h => others_bigger a ⟨h, has⟩

Premises used: And.intro
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y
neg : ∀ (a₀ : α) (ha₀s : a₀ ∈ s), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ha₀s⟩ := hs
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
⟨a₀, ha₀s, fun a ha => all_top a ha (f a₀)⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
exact ⟨a₀, ha₀s, fun a ha => all_top a ha (f a₀)⟩
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : Nonempty α
inst_1 : LinearOrder β
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ (a₀ : α), ∀ (a : α), f a₀ ≤ f a

Tactic:
let ⟨a₀, _, ha₀⟩ := hf.exists_within_forall_le univ_nonempty
  ⟨a₀, fun a => ha₀ a (mem_univ _)⟩

Premises used: Set.univ_nonempty, Exists, Filter.Tendsto.exists_within_forall_le, Exists.intro, Set.mem_univ, _private.0.Filter.Tendsto.exists_forall_le.match_1
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atBot
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀

Tactic:
@Filter.Tendsto.exists_within_forall_le _ βᵒᵈ _ _ hs _ hf

Premises used: Filter.Tendsto.exists_within_forall_le
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : Nonempty α
inst_1 : LinearOrder β
f : α → β
hf : Tendsto f cofinite atBot
⊢ ∃ (a₀ : α), ∀ (a : α), f a ≤ f a₀

Tactic:
@Filter.Tendsto.exists_forall_le _ βᵒᵈ _ _ _ hf

Premises used: Filter.Tendsto.exists_forall_le
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
hf : Surjective f
⊢ cofinite ≤ map f cofinite

Tactic:
fun _ h => .of_preimage h hf

Premises used: Set.Mem, setOf, Set.Finite, Set.Finite.of_preimage
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
⊢ Tendsto f cofinite cofinite

Tactic:
fun _ h => h.preimage hf.injOn

Premises used: Set.Mem, Function.Injective.injOn, setOf, Set.Finite, Set.preimage, Filter.Tendsto, Not, Set.Finite.preimage
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
hf : ∀ (b : β), Finite.{u_2 + 1} (↑(f ⁻¹' {b}) : Type u_2)
⊢ Tendsto f cofinite cofinite

Tactic:
fun _ h => h.preimage' fun b _ ↦ hf b

Premises used: Set.Mem, setOf, Set.Finite, Set.preimage, Filter.Tendsto, Not, Set.Finite.preimage'
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
⊢ comap f cofinite = cofinite

Tactic:
(comap_cofinite_le f).antisymm hf.tendsto_cofinite.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.comap_cofinite_le, LE.le.antisymm, Function.Injective.tendsto_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
f : ℕ → ℕ
hf : Injective f
⊢ Tendsto f atTop atTop

Tactic:
Nat.cofinite_eq_atTop ▸ hf.tendsto_cofinite

Premises used: Eq.rec, Function.Injective.tendsto_cofinite, Nat.cofinite_eq_atTop
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : α → β
a : α
b : β
u : α
hu : Membership.mem (γ := Set α) {a}ᶜ u
⊢ update (β := fun (a : α) ↦ β) f a b u = f u

Tactic:
Function.update_of_ne hu _ _

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : α → β
a : α
b : β
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {a}ᶜ x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ update (β := fun (a : α) ↦ β) f a b x = f x) x} x}
      a_1
h₁ h₂ : ∀ (u : α) (hu : Membership.mem (γ := Set α) {a}ᶜ u), update (β := fun (a : α) ↦ β) f a b u = f u
⊢ update (β := fun (a : α) ↦ β) f a b =ᶠ[𝓟 {a}ᶜ] f

Tactic:
filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _

Premises used: Filter.mem_principal_self
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : α → β
a : α
b : β
⊢ LE.le (α := Filter α) cofinite (𝓟 {a}ᶜ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
rw : (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ (i : Set α) (_ : i ∈ f), a ∉ i
⊢ f ≤ cofinite ↔ f.ker = ∅

Tactic:
rw [le_cofinite_iff_compl_singleton_mem, ker_def, iInter₂_eq_empty_iff]

Premises used: Filter.le_cofinite_iff_compl_singleton_mem, Filter.ker_def, Set.iInter₂_eq_empty_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
x : α
h : {x}ᶜ ∈ f
⊢ x ∉ {x}ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
x : α
h : ∃ (i : Set α) (_ : i ∈ f), x ∉ i
s : Set α
hs : s ∈ f
hx : x ∉ s
⊢ s ⊆ {x}ᶜ

Tactic:
simpa using hx
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ (i : Set α) (_ : i ∈ f), a ∉ i

Tactic:
exact forall_congr' fun x => ⟨fun h => ⟨{x}ᶜ, h, by simp⟩,
    fun ⟨s, hs, hx⟩ => mem_of_superset hs (by simpa using hx)⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
rw : f.ker = ∅ ↔ f.kerᶜ ∈ f
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f

Tactic:
rw [← Coheyting.inf_hnot_self, inf_eq_left, le_cofinite_iff_ker,
    Filter.hnot_def, le_principal_iff]

Premises used: Filter.le_principal_iff, Coheyting.inf_hnot_self, le_cofinite_iff_ker, Filter.hnot_def, inf_eq_left
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
mp : f.ker = ∅ → f.kerᶜ ∈ f
mpr : f.kerᶜ ∈ f → f.ker = ∅
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
h : f.ker = ∅
⊢ f.kerᶜ ∈ f

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
mpr : ∀ (x : α), x ∉ f.ker
⊢ f.ker = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
hx : x ∈ f.ker
⊢ False

Tactic:
hx f.kerᶜ h hx

Premises used: Compl.compl, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
hx : x ∈ f.ker
⊢ False

Tactic:
exact hx f.kerᶜ h hx

Premises used: Compl.compl, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ Coheyting.boundary f ≤ cofinite

Tactic:
le_cofinite_iff_boundary.2 (Coheyting.boundary_boundary f)

Premises used: Coheyting.boundary_boundary, Iff.mpr, le_cofinite_iff_boundary
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
⊢ Coheyting.boundary (𝓟 s) = ⊥

Tactic:
simp [← Coheyting.inf_hnot_self]

Premises used: Coheyting.inf_hnot_self
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2

Tactic:
⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩

Premises used: Prod.mk, Coheyting.boundary, ExistsUnique, And.intro, Exists.intro, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
refine_1 : (f.ker, Coheyting.boundary f).2 ≤ cofinite
refine_2 : Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2
refine_3 : f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
refine_4 :
  ∀ (q : Set α × Filter α)
    (hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q),
    q = (f.ker, Coheyting.boundary f)
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2

Tactic:
refine ⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).2 ≤ cofinite

Tactic:
boundary_le_cofinite f

Premises used: Set.Mem, boundary_le_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).2 ≤ cofinite

Tactic:
exact boundary_le_cofinite f

Premises used: boundary_le_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
refine_2 : (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2
⊢ Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2

Tactic:
rw [disjoint_principal_left]

Premises used: Filter.disjoint_principal_left
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2

Tactic:
mem_inf_of_right (mem_principal_self f.kerᶜ)

Premises used: Filter.mem_principal_self, Set.Mem, Compl.compl, Filter.mem_inf_of_right, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2

Tactic:
exact mem_inf_of_right (mem_principal_self f.kerᶜ)

Premises used: Filter.mem_principal_self, Compl.compl, Filter.mem_inf_of_right, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
refine_3 : f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₁ : f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₂ : f = ￢￢f ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₃ refine_3₄ : f = f
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2

Tactic:
rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]

Premises used: compl_compl, Coheyting.hnot_hnot_sup_boundary, Filter.hnot_def, Filter.hnot_principal, Filter.ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ f.ker = (𝓟 q.1 ⊔ q.2).ker

Tactic:
have hqk := congrArg Filter.ker hq.2.2
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
⊢ f.ker = q.1

Tactic:
rw [ker_sup, ker_principal, le_cofinite_iff_ker.mp hq.1, union_empty] at hqk

Premises used: Set.union_empty, Filter.ker_principal, Filter.ker_sup, le_cofinite_iff_ker, And.left, Iff.mp
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)

Premises used: Prod.mk, le_inf, le_antisymm, congrArg₂, Eq.symm
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : q.2 ≤ f
refine_4₁ : q.2 ≤ ￢f
refine_4₂ : Coheyting.boundary f ≤ q.2
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)

Premises used: Prod.mk, le_inf, le_antisymm, congrArg₂, Eq.symm
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : q.2 ≤ 𝓟 q.1 ⊔ q.2
⊢ q.2 ≤ f

Tactic:
rw [hq.2.2]

Premises used: And.right
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ 𝓟 q.1 ⊔ q.2

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ 𝓟 q.1 ⊔ q.2

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : Disjoint (𝓟 q.1) q.2
⊢ q.2 ≤ ￢f

Tactic:
rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]

Premises used: Filter.le_principal_iff, Filter.disjoint_principal_left, Filter.hnot_def
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Disjoint (𝓟 q.1) q.2

Tactic:
hq.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Disjoint (𝓟 q.1) q.2

Tactic:
exact hq.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : Coheyting.boundary q.2 ≤ q.2
⊢ Coheyting.boundary f ≤ q.2

Tactic:
grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]

Premises used: boundary_principal, bot_sup_eq, Coheyting.boundary_sup_le, And.right
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary q.2 ≤ q.2

Tactic:
Coheyting.boundary_le

Premises used: Coheyting.boundary_le
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary q.2 ≤ q.2

Tactic:
exact Coheyting.boundary_le

Premises used: Coheyting.boundary_le
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
f : Filter α
⊢ ∃ (s : Set α), ∃ g ≤ cofinite, Disjoint (𝓟 s) g ∧ f = 𝓟 s ⊔ g

Tactic:
Prod.exists.mp (existsUnique_eq_principal_sup_free f).exists

Premises used: ExistsUnique.exists, Set.Mem, existsUnique_eq_principal_sup_free, setOf, Iff.mp, Prod.exists
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
S : Set (Set α)
hSc : S.Countable
⊢ ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l

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

Premises used: CountableInterFilter.countable_sInter_mem, Set.sInter_subset_of_mem, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
s : ι → Set α
⊢ ⋂ (i : ι), s i ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_mem_range

Premises used: Set.forall_mem_range, Eq.rec, Set.countable_range, Set.sInter_range, Iff.trans, countable_sInter_mem
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
rw : ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
⊢ ⋂ (i : ι), ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
rw [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
haveI :
  ∀ (this : Encodable (↑S : Type u_4)), ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
haveI := hS.toEncodable
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable (↑S : Type u_4)
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
countable_iInter_mem.trans Subtype.forall

Premises used: countable_iInter_mem, Subtype.forall, Iff.trans
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable (↑S : Type u_4)
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact countable_iInter_mem.trans Subtype.forall

Premises used: countable_iInter_mem, Subtype.forall, Iff.trans
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simpa only [Filter.Eventually, setOf_forall] using
    @countable_iInter_mem _ _ l _ _ fun i => { x | p x i }

Premises used: countable_iInter_mem, Filter.Eventually, Set.setOf_forall
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simpa only [Filter.Eventually, setOf_forall] using
    @countable_bInter_mem _ l _ _ _ hS fun i hi => { x | p x i hi }

Premises used: countable_bInter_mem, Filter.Eventually, Set.setOf_forall
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Finset ι
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
eventually_countable_ball S.countable_toSet

Premises used: eventually_countable_ball, Finset.countable_toSet
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
s t : ι → Set α
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

Tactic:
(eventually_countable_forall.2 h).mono fun _ hst hs => mem_iUnion.2 <| (mem_iUnion.1 hs).imp hst

Premises used: Iff.mpr, Set.mem_iUnion, Exists.imp, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE, eventually_countable_forall
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
s t : ι → Set α
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

Tactic:
(EventuallyLE.countable_iUnion fun i => (h i).le).antisymm
    (EventuallyLE.countable_iUnion fun i => (h i).symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm, Filter.EventuallyLE.countable_iUnion
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
simp : ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
⊢ ⋃ (i : ι), ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

Tactic:
simp only [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
haveI :
  ∀ (this : Encodable (↑S : Type u_4)),
    ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
⊢ ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
haveI := hS.toEncodable
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable (↑S : Type u_4)
⊢ ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
EventuallyLE.countable_iUnion fun i => h i i.2

Premises used: Subtype.val, Filter.EventuallyLE.countable_iUnion, Subtype.property
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable (↑S : Type u_4)
⊢ ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯

Tactic:
exact EventuallyLE.countable_iUnion fun i => h i i.2
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi
⊢ ⋃ (i : ι), ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h

Tactic:
(EventuallyLE.countable_bUnion hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.countable_bUnion hS fun i hi => (h i hi).symm.le)

Premises used: Filter.EventuallyLE.countable_bUnion, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
s t : ι → Set α
h : ∀ (i : ι), s i ≤ᶠ[l] t i
⊢ ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

Tactic:
(eventually_countable_forall.2 h).mono fun _ hst hs =>
    mem_iInter.2 fun i => hst _ (mem_iInter.1 hs i)

Premises used: Iff.mpr, Set.mem_iInter, Filter.Eventually.mono, Iff.mp, Filter.EventuallyLE, eventually_countable_forall
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
inst : CountableInterFilter l
inst_1 : Countable ι
s t : ι → Set α
h : ∀ (i : ι), s i =ᶠ[l] t i
⊢ ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

Tactic:
(EventuallyLE.countable_iInter fun i => (h i).le).antisymm
    (EventuallyLE.countable_iInter fun i => (h i).symm.le)

Premises used: Filter.EventuallyLE.countable_iInter, Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.Order.Filter.CountableInter
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
simp : ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
⊢ ⋂ (i : ι), ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter