-- Mathlib/Order/LiminfLimsup.lean
theorem exists_forall_mem_of_hasBasis_mem_blimsup {l : Filter β} {b : ι → Set β} {q : ι → Prop}
    (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ blimsup u l p) :
    ∃ f : { i | q i } → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Proof state:
case refine_2
α : 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 ∈ 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) ⋯) i) ∧ (fun i => g (b ↑i) ⋯) i ∈ b ↑i

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

Result:
no goals

Proof state:
α : 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 ∈ ⨅ 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

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

Result:
α : 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 ∈ 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

Proof state:
case refine_1
α : 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 ∈ 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) ⋯) i)

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

Result:
no goals

Proof state:
α : 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
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

Tactic:
rw [blimsup_eq_iInf_biSup] at hx

Result:
α : 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 ∈ ⨅ 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

Proof state:
α : 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 ∈ 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

Tactic:
choose g hg hg' using hx

Result:
α : 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 ∈ 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

Proof state:
α : 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 ∈ 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

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

Result:
case refine_1
α : 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 ∈ 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) ⋯) i)

case refine_2
α : 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 ∈ 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) ⋯) i) ∧ (fun i => g (b ↑i) ⋯) i ∈ b ↑i