α : Type u_2
β✝ : Type ?u.3743
γ : Type u_4
ι✝ : Sort ?u.3749
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Type u_1
p : ι → Prop
s : ι → Set α
f : Filter α
hf : HasBasis f p s
β : ι → Type u_3
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s i)) (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t
α : Type u_2
β✝ : Type ?u.3743
γ : Type u_4
ι✝ : Sort ?u.3749
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Type u_1
p : ι → Prop
s : ι → Set α
f : Filter α
hf : HasBasis f p s
β : ι → Type u_3
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s i)) (pg i) (sg i)
gm : Monotone g
⊢ HasBasis (Filter.lift f g) (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
refine' ⟨fun t => (hf.mem_lift_iff hg gm).trans _⟩
no goals
α : Type u_2
β✝ : Type ?u.3743
γ : Type u_4
ι✝ : Sort ?u.3749
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Type u_1
p : ι → Prop
s : ι → Set α
f : Filter α
hf : HasBasis f p s
β : ι → Type u_3
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s i)) (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t
simp [Sigma.exists, and_assoc, exists_and_left]