trouble defining filter base

Stream: general

[Bernd Losert]

I have the following code:

import tactic
import order.filter.partial
import order.filter.ultrafilter
import order.filter.bases
import algebra.support

noncomputable theory
open set function filter classical
open_locale classical filter

variables {X Y Z : Type*}

lemma ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
∃ 𝒰 : ultrafilter X, 𝒰.map f = 𝒱 ∧ A ∈ 𝒰 := begin
  let ℬ : filter_basis X := {
    sets := { f ⁻¹' V ∩ A | V ∈ 𝒱 }, -- WHY DOES THIS NOT WORK?
    nonempty := sorry,
    inter_sets := sorry,
  },
  let ℱ := ℬ.filter,
  haveI : ℱ.ne_bot := sorry,
  let 𝒰 := ultrafilter.of ℱ,
  use 𝒰,
  have h : 𝒰.map f = 𝒱, sorry,
  have h' : A ∈ 𝒰, sorry,
  exact and.intro h h',
end

I can't figure out what the problem is though.

[Reid Barton]

Sadly, the syntax you are trying to use there simply does not exist.

[Bernd Losert]

Oh. What is the correct syntax then?

[Reid Barton]

You can write sets := { W | ∃ V ∈ 𝒱, W = f ⁻¹' V ∩ A },

[Reid Barton]

The thing before the | has to be a variable

[Bernd Losert]

Ah, I see. For some reason, I thought the set comprehension syntax was more flexible.

[Yaël Dillies]

Reid Barton said:

The thing before the | has to be a variable

or a ∈

[Adam Topaz]

That's not completely true... e.g.

import data.set.basic

variables {α β : Type*} (f : α → β) (S : set α)

def foo : set β := { (f x) | x ∈ S}

example : foo f S = { t | ∃ x ∈ S, f x = t } := rfl

[Bernd Losert]

Aha. So I tried { (f ⁻¹' V ∩ A) | V ∈ 𝒱 }, and that works.

[Reid Barton]

Wait really??

[Reid Barton]

Aha, a "new" feature (added around 3.18 apparently)

[Adam Topaz]

Yep! This syntax was added fairly recently

[Bernd Losert]

It's weird that you have to add parentheses though.

[Reid Barton]

I assume it's because a variable is also an expression, but if we interpret it as an expression then the translation changes (it involves an existential and an equality).