case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b
α : Type u
⊢ ∀ (t₁ : Set (Ultrafilter α)),
    t₁ ∈ ultrafilterBasis α →
      ∀ (t₂ : Set (Ultrafilter α)),
        t₂ ∈ ultrafilterBasis α →
          ∀ (x : Ultrafilter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
no goals
case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b
refine' ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv => ⟨_, _⟩⟩ <;> apply mem_of_superset hv <;>
  simp [inter_subset_right a b]