α : Type u_1
β : Type ?u.181072
γ : Type ?u.181075
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite pᶜ = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
α : Type u_1
β : Type ?u.181072
γ : Type ?u.181075
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}
rw [← compl_inj_iff]
α : Type u_1
β : Type ?u.181072
γ : Type ?u.181075
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ {x | Set.Infinite {n | p n ∧ x ∈ s nᶜ}} = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
α : Type u_1
β : Type ?u.181072
γ : Type ?u.181075
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite pᶜ = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
  cofinite.blimsup_set_eq]
no goals
α : Type u_1
β : Type ?u.181072
γ : Type ?u.181075
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ {x | Set.Infinite {n | p n ∧ x ∈ s nᶜ}} = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
rfl