α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ (s : Set β) (_ : s ∈ l), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
rw [blimsup_eq_iInf_biSup] at hx
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β), i ∈ l → ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ (s : Set β) (_ : s ∈ l), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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 : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β), i ∈ l → ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
choose g hg hg' using hx
case refine'_1
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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}
⊢ x ∈ u ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i)

case refine'_2
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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}
⊢ p ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i) ∧ (fun i => g (b ↑i) (_ : b ↑i ∈ l)) i ∈ b ↑i
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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 : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
refine' ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨_, _⟩⟩
no goals
case refine'_1
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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}
⊢ x ∈ u ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i)
exact hg' (b i) (hl.mem_of_mem i.2)
no goals
case refine'_2
α : Type u_3
β : Type u_1
γ : Type ?u.183305
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → 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}
⊢ p ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i) ∧ (fun i => g (b ↑i) (_ : b ↑i ∈ l)) i ∈ b ↑i
exact hg (b i) (hl.mem_of_mem i.2)