α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
⊢ HasBasis l (fun i => p i ∧ q i) s
refine' ⟨fun t => ⟨fun ht => _, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
case intro.intro
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
case intro.intro
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.23444
γ : Type ?u.23447
ι : Sort u_2
ι' : Sort ?u.23453
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩