case refine'_1
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ DirectedOn ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) f.sets

case refine'_2
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ s ∈ Filter.lift f g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
refine' (mem_biInf_of_directed _ ⟨univ, univ_sets _⟩).trans _
case refine'_1
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z, z ∈ f.sets ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₁ z ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₂ z
case refine'_1
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ DirectedOn ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) f.sets
intro t₁ ht₁ t₂ ht₂
no goals
case refine'_1
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z, z ∈ f.sets ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₁ z ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₂ z
exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm <| inter_subset_left _ _, gm <| inter_subset_right _ _⟩
case refine'_2
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ s ∈ g (s✝ i)
case refine'_2
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
simp only [← (hg _).mem_iff]
no goals
case refine'_2
α : Type u_2
β✝ : Type ?u.2792
γ : Type u_4
ι✝ : Sort ?u.2798
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort 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
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ s ∈ g (s✝ i)
exact hf.exists_iff fun t₁ t₂ ht H => gm ht H