awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
refine_2 :
  ∀ (a : β),
    Membership.mem (γ := Set β) {x : β | (fun (a : β) ↦ a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a) x} a
refine_2₁ refine_2₂ : ∀ (a : β) (h : a ∉ s), s.piecewise (β := fun (a : β) ↦ α) u v a = v a
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise (β := fun (a : β) ↦ α) u v a = v a

Tactic:
filter_upwards with _ h using by simp [h]
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst_1 : DecidablePred fun (x : β) ↦ x ∈ s
v : (i : β) → α
⊢ liminf (s.piecewise (β := fun (a : β) ↦ α) u v) f =
    (bliminf u f fun (x : β) ↦ x ∈ s) ⊓ bliminf v f fun (x : β) ↦ x ∉ s

Tactic:
limsup_piecewise (α := αᵒᵈ)

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.bliminf, Filter.limsup_piecewise, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
simp : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a) (⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
⊢ a ⊔ limsup u f = limsup (fun (x : β) ↦ a ⊔ u x) f

Tactic:
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]

Premises used: iSup_sup_eq, Filter.limsup_eq_iInf_iSup, sup_iInf₂_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
e_s :
  Eq (α := Set β → α) (fun (i : Set β) ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) fun (s : Set β) ↦
    ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a) (⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)

Tactic:
congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
e_s :
  ∀ (s : Set β), Eq.{u_1 + 1} (α := α) (⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a) (⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)
⊢ Eq (α := Set β → α) (fun (i : Set β) ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) fun (s : Set β) ↦
    ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
ext s
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
e_s : Eq.{u_1 + 1} (α := s ∈ f → α) (fun (j : s ∈ f) ↦ a ⊔ ⨆ a ∈ s, u a) fun (x : s ∈ f) ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
⊢ Eq.{u_1 + 1} (α := α) (⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a) (⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x)

Tactic:
congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
e_s : ∀ (hs : s ∈ f), a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
⊢ Eq.{u_1 + 1} (α := s ∈ f → α) (fun (j : s ∈ f) ↦ a ⊔ ⨆ a ∈ s, u a) fun (x : s ∈ f) ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
ext hs
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
hs : s ∈ f
e_s : a = ⨆ x ∈ s, a
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
congr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ x ∈ s, a

Tactic:
(biSup_const (nonempty_of_mem hs)).symm

Premises used: Filter.nonempty_of_mem, biSup_const, Eq.symm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ x ∈ s, a

Tactic:
exact (biSup_const (nonempty_of_mem hs)).symm

Premises used: Filter.nonempty_of_mem, biSup_const, Eq.symm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ a ⊓ liminf u f = liminf (fun (x : β) ↦ a ⊓ u x) f

Tactic:
sup_limsup (α := αᵒᵈ) a

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.sup_limsup, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
simp : a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
⊢ a ⊔ liminf u f = liminf (fun (x : β) ↦ a ⊔ u x) f

Tactic:
simp only [liminf_eq_iSup_iInf]

Premises used: Filter.liminf_eq_iSup_iInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
rw : Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)
⊢ a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Tactic:
rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]

Premises used: Set.univ, sup_comm, Exists.intro, Filter.univ_mem, biSup_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, ⨅ i_1 ∈ i, u i_1 ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a) (⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1)

Tactic:
simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

Premises used: sup_comm, iInf₂_sup_eq
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊓ limsup u f = limsup (fun (x : β) ↦ a ⊓ u x) f

Tactic:
sup_liminf (α := αᵒᵈ) a

Premises used: Filter.limsSup, setOf, Filter.limsup, OrderDual, Filter.sup_liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Premises used: compl_iSup, compl_iInf, Filter.liminf_eq_iSup_iInf, Filter.limsup_eq_iInf_iSup, Function.comp_apply
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Premises used: compl_iSup, compl_iInf, Filter.liminf_eq_iSup_iInf, Filter.limsup_eq_iInf_iSup, Function.comp_apply
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
simp : (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
⊢ limsup u f \ a = limsup (fun (b : β) ↦ u b \ a) f

Tactic:
simp only [limsup_eq_iInf_iSup, sdiff_eq]

Premises used: sdiff_eq, Filter.limsup_eq_iInf_iSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
rw : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
⊢ (⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]

Premises used: Set.univ, Exists.intro, biInf_inf, Filter.univ_mem
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
simp_rw : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, aᶜ ⊓ ⨆ a ∈ i, u a) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
simp_rw₁ : Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, ⨆ i_1 ∈ i, aᶜ ⊓ u i_1) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)
⊢ Eq.{u_1 + 1} (α := α) (⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ) (⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ)

Tactic:
simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

Premises used: inf_iSup₂_eq, inf_comm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ liminf u f \ a = liminf (fun (b : β) ↦ u b \ a) f

Tactic:
simp only [sdiff_eq, inf_comm _ aᶜ, inf_liminf]

Premises used: Compl.compl, sdiff_eq, inf_comm, Filter.inf_liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
rw : (a \ limsup u f)ᶜ = (liminf (fun (b : β) ↦ a \ u b) f)ᶜ
⊢ a \ limsup u f = liminf (fun (b : β) ↦ a \ u b) f

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst_1 : f.NeBot
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun (b : β) ↦ a \ u b) f)ᶜ

Tactic:
simp only [sdiff_eq, liminf_compl, comp_def, compl_inf, compl_compl, sup_limsup]

Premises used: compl_inf, compl_compl, sdiff_eq, Filter.sup_limsup, Filter.liminf_compl, Function.comp_def
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
rw : (a \ liminf u f)ᶜ = (limsup (fun (b : β) ↦ a \ u b) f)ᶜ
⊢ a \ liminf u f = limsup (fun (b : β) ↦ a \ u b) f

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun (b : β) ↦ a \ u b) f)ᶜ

Tactic:
simp only [sdiff_eq, limsup_compl, comp_def, compl_inf, compl_compl, sup_liminf]

Premises used: compl_inf, compl_compl, Filter.limsup_compl, sdiff_eq, Function.comp_def, Filter.sup_liminf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
h : ∃ (i : Set ι) (_ : i ∈ 𝓕), ∀ (i_1 : ι) (i : i_1 ∈ i), a ∈ s i_1
S : Set ι
hS : S ∈ 𝓕
hS' : ∀ (i : ι) (i_1 : i ∈ S), a ∈ s i
⊢ S ⊆ {x : ι | (fun (i : ι) ↦ a ∈ s i) x}

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
h : ∀ᶠ (i : ι) in 𝓕, a ∈ s i
tauto tauto₁ tauto₂ : ∀ (i : ι), Membership.mem (γ := Set ι) {i : ι | a ∈ s i} i → a ∈ s i
⊢ ∀ (i : ι) (i_1 : Membership.mem (γ := Set ι) {i : ι | a ∈ s i} i), a ∈ s i

Tactic:
tauto
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simpa only [liminf_eq_iSup_iInf, iSup_eq_iUnion, iInf_eq_iInter, mem_iUnion, mem_iInter]
    using ⟨fun ⟨S, hS, hS'⟩ ↦ mem_of_superset hS (by tauto), fun h ↦ ⟨{i | a ∈ s i}, h, by tauto⟩⟩

Premises used: Set.iInf_eq_iInter, Set.mem_iUnion, Set.iSup_eq_iUnion, Set.mem_iInter, Filter.liminf_eq_iSup_iInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simp only [Filter.Frequently, iff_not_comm, ← mem_compl_iff, limsup_compl, comp_apply,
    mem_liminf_iff_eventually_mem]

Premises used: iff_not_comm, Filter.limsup_compl, Filter.Frequently, Function.comp_apply, Set.mem_compl_iff, Filter.mem_liminf_iff_eventually_mem
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
simp :
  Eq.{u_1 + 1} (α := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}})
    {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
⊢ blimsup s cofinite p = {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}

Tactic:
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]

Premises used: Filter.blimsup_eq, Set.le_eq_subset, Filter.eventually_cofinite, exists_prop, Set.sInf_eq_sInter, Classical.not_forall
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
      Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
⊢ Eq.{u_1 + 1} (α := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}})
    {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}

Tactic:
ext x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x

Tactic:
⟨fun h => ?_, fun hx t h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h :
  ∀ (h : Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x),
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
h₁ :
  ∀ (hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x) (t : Set α)
    (h : Membership.mem (γ := Set (Set α)) {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}} t), x ∈ t
⊢ Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x ↔
    Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x

Tactic:
refine ⟨fun h => ?_, fun hx t h => ?_⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : Membership.mem (γ := Set α) (⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}) x
h₁ :
  ∀ (h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}),
    x ∉ ⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}
⊢ Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x

Tactic:
contrapose h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
t : Set α
h : Membership.mem (γ := Set (Set α)) {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}} t
h₁ : ∀ (h : x ∉ t), t ∉ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}
⊢ x ∈ t

Tactic:
contrapose h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
h₁ : ∃ (x_1 : Set α), Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ x_1} ∧ x ∉ x_1
⊢ x ∉ ⋂₀ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}

Tactic:
simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]

Premises used: Set.mem_setOf_eq, exists_prop, Set.mem_sInter, Classical.not_forall
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
⊢ Set.Finite.{u_4} (α := ι) {x_1 : ι | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}

Tactic:
simpa using h
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
⊢ x ∉ {x}ᶜ

Tactic:
simp
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}}
⊢ ∃ (x_1 : Set α), Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ x_1} ∧ x ∉ x_1

Tactic:
exact ⟨{x}ᶜ, by simpa using h, by simp⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
t : Set α
h : x ∉ t
⊢ t ∉ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}

Tactic:
hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩

Premises used: Set.Infinite.mono, Set.Mem, setOf, Set.Finite, And.intro, Set.Infinite
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : Membership.mem (γ := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ s n}} x
t : Set α
h : x ∉ t
⊢ t ∉ {a : Set α | Set.Finite.{u_4} (α := ι) {x : ι | p x ∧ ¬s x ⊆ a}}

Tactic:
exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
rw : (bliminf s cofinite p)ᶜ = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ
⊢ bliminf s cofinite p = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
simp :
  Eq.{u_1 + 1} (α := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ (s n)ᶜ}}
    {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ
⊢ (bliminf s cofinite p)ᶜ = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ

Tactic:
simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
    cofinite.blimsup_set_eq]

Premises used: Filter.blimsup_eq_iInf_biSup, compl_iSup, compl_iInf, Filter.cofinite.blimsup_set_eq, Filter.bliminf_eq_iSup_biInf
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | p n ∧ x ∈ (s n)ᶜ}}
    {x : α | Set.Finite.{u_4} (α := ι) {n : ι | p n ∧ x ∉ s n}}ᶜ

Tactic:
rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ limsup s cofinite = {x : α | Set.Infinite.{u_4} (α := ι) {n : ι | x ∈ s n}}

Tactic:
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

Premises used: Filter.blimsup_true, Filter.cofinite, Filter.cofinite.blimsup_set_eq, true_and
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ liminf s cofinite = {x : α | Set.Finite.{u_4} (α := ι) {n : ι | x ∉ s n}}

Tactic:
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

Premises used: Filter.bliminf_true, Filter.cofinite.bliminf_set_eq, Filter.cofinite, true_and
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ Membership.mem (γ := Set α) (⨅ s ∈ l, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) x

Tactic:
rw [blimsup_eq_iInf_biSup] at hx

Premises used: Filter.blimsup_eq_iInf_biSup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : Membership.mem (γ := Set α) (⨅ s ∈ l, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b) x
⊢ ∀ (i : Set β) (i_1 : i ∈ l), ∃ (i_2 : β), (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2

Tactic:
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx

Premises used: Set.iInf_eq_iInter, Set.mem_iUnion, Set.iSup_eq_iUnion, exists_prop, Set.mem_iInter
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β) (i_1 : i ∈ l), ∃ (i_2 : β), (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
choose :
  ∀ (g : (i : Set β) → (i : i ∈ l) → β) (hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i)
    (hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)),
    ∃ (f : (↑{i : ι | q i} : Type u_4) → β),
      ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)

Tactic:
choose g hg hg' using hx
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)

Tactic:
⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, Subtype.val, Filter.HasBasis.mem_of_mem, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
refine_1 : ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i)
refine_2 :
  ∀ (i : (↑{i : ι | q i} : Type u_4)),
    p ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i) ∧
      (fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i ∈ b (↑i : ι)
⊢ ∃ (f : (↑{i : ι | q i} : Type u_4) → β), ∀ (i : (↑{i : ι | q i} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)

Tactic:
refine ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : (↑{i : ι | q i} : Type u_4)
⊢ x ∈ u ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i)

Tactic:
hg' (b i) (hl.mem_of_mem i.2)

Premises used: Set.Mem, Subtype.val, Filter.HasBasis.mem_of_mem, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : (↑{i : ι | q i} : Type u_4)
⊢ x ∈ u ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i)

Tactic:
exact hg' (b i) (hl.mem_of_mem i.2)

Premises used: Subtype.val, Filter.HasBasis.mem_of_mem, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : (↑{i : ι | q i} : Type u_4)
⊢ p ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i) ∧
    (fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i ∈ b (↑i : ι)

Tactic:
hg (b i) (hl.mem_of_mem i.2)

Premises used: Set.Mem, Subtype.val, Filter.HasBasis.mem_of_mem, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → (i : i ∈ l) → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : (↑{i : ι | q i} : Type u_4)
⊢ p ((fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i) ∧
    (fun (i : (↑{i : ι | q i} : Type u_4)) ↦ g (b (↑i : ι)) ⋯) i ∈ b (↑i : ι)

Tactic:
exact hg (b i) (hl.mem_of_mem i.2)

Premises used: Subtype.val, Filter.HasBasis.mem_of_mem, Subtype.property
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun (x : ι) ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
obtain :
  ∀ (f : (↑{i : ι | True} : Type u_4) → β)
    (hf : ∀ (i : (↑{i : ι | True} : Type u_4)), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b (↑i : ι)),
    ∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
⊢ ∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx

Premises used: Filter.exists_forall_mem_of_hasBasis_mem_blimsup