case intro
α : Type u_3
β : Type u_1
γ : Type ?u.185252
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
α : Type u_3
β : Type u_1
γ : Type ?u.185252
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
no goals
case intro
α : Type u_3
β : Type u_1
γ : Type ?u.185252
ι : Type u_2
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩