α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
case h
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} ↔ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
ext x
case h.refine'_1
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}

case h.refine'_2
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : ¬x ∈ t
⊢ ¬t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
case h
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} ↔ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
refine' ⟨fun h => _, fun hx t h => _⟩ <;> contrapose! h
case h.refine'_1
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ∃ x_1, Set.Finite {x | p x ∧ ¬s x ⊆ x_1} ∧ ¬x ∈ x_1
case h.refine'_1
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
no goals
case h.refine'_1
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ∃ x_1, Set.Finite {x | p x ∧ ¬s x ⊆ x_1} ∧ ¬x ∈ x_1
exact ⟨{x}ᶜ, by simpa using h, by simp⟩
no goals
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ Set.Finite {x_1 | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}
simpa using h
no goals
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ {x}ᶜ
simp
no goals
case h.refine'_2
α : Type u_1
β : Type ?u.177596
γ : Type ?u.177599
ι : Type u_2
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : ¬x ∈ t
⊢ ¬t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩