case intro.intro
ι : Sort ?u.640
α : Type u_1
β : Type ?u.646
X : Type ?u.649
Y : Type ?u.652
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
ι : Sort ?u.640
α : Type u_1
β : Type ?u.646
X : Type ?u.649
Y : Type ?u.652
⊢ ∀ (t₁ : Set (Filter α)),
    t₁ ∈ range (Iic ∘ 𝓟) →
      ∀ (t₂ : Set (Filter α)),
        t₂ ∈ range (Iic ∘ 𝓟) → ∀ (x : Filter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
no goals
case intro.intro
ι : Sort ?u.640
α : Type u_1
β : Type ?u.646
X : Type ?u.649
Y : Type ?u.652
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
no goals
ι : Sort ?u.640
α : Type u_1
β : Type ?u.646
X : Type ?u.649
Y : Type ?u.652
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)
simp