rw using an iff

Stream: general

[Bernd Losert]

Is it possible to use rw with an iff theorem? I'm getting an error when I try to use it.

[Kyle Miller]

Yes, rw can rewrite using iffs and equalities. It would be helpful if you posted a #mwe for this.

[Bernd Losert]

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

noncomputable theory
open set function filter classical
open_locale classical filter

variables {X Y Z : Type*}

lemma ultrafilter_comap_ne_bot (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) : (comap f 𝒱).ne_bot := begin
  rw filter.forall_mem_nonempty_iff_ne_bot
end

[Patrick Johnson]

Rewrite it in the other direction:

rw ←filter.forall_mem_nonempty_iff_ne_bot

[Bernd Losert]

Ah, it works. I remember trying that and it gave me an error. Weird.

[Bernd Losert]

So now I have this, and it's giving me an error that I don't know how to fix:

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

noncomputable theory
open set function filter classical
open_locale classical filter

variables {X Y Z : Type*}

lemma ultrafilter_comap_ne_bot (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) : (comap f 𝒱).ne_bot := begin
  rw ← filter.forall_mem_nonempty_iff_ne_bot,
  assume A : set X,
  assume h' : A ∈ comap f 𝒱,
  have : (f '' A).nonempty := ultrafilter.nonempty_of_mem h,
end

[Bernd Losert]

Ah, I guess it's because the A I'm using is not the same A from the statement of the lemma.

[Bernd Losert]

Proving this is giving me more trouble that I thought. This is the proof that I want to write in Lean:

Since f '' A ∈ 𝒱, then for every V ∈ 𝒱, we have that f '' A ∩ V ≠ Ø, hence f ⁻¹' V ≠ Ø, hence Ø ∉ comap f 𝒱 , hence comap f 𝒱.ne_bot

[Bernd Losert]

Hmm... I think I need an extra condition: nonempty A.

[Kyle Miller]

This doesn't seem to be true: "since f '' A ∩ V ≠ Ø then f ⁻¹' V ≠ Ø". If f is surjective, for example, it would be.

[Kevin Buzzard]

Doesn't the a in A work?

[Patrick Massot]

lemma ultrafilter_comap_ne_bot (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
  (comap f 𝒱).ne_bot :=
begin
  apply comap_ne_bot,
  intros U U_in,
  rcases (ultrafilter.nonempty_of_mem $ inter_mem h U_in) with ⟨-, ⟨x, h, rfl⟩, h'⟩,
  tauto,
end

[Patrick Massot]

If you want to put this in mathlib then you should fix the binders, something like:

lemma ultrafilter.comap_ne_bot (𝒱 : ultrafilter Y) {f : X → Y} {A : set X}  (h : f '' A ∈ 𝒱) :
  (comap f 𝒱).ne_bot :=
begin
  apply comap_ne_bot (λ U U_in, _),
  rcases (filter.nonempty_of_mem $ inter_mem h U_in) with ⟨-, ⟨x, -, rfl⟩, h⟩,
  exact ⟨x, h⟩
end

[Patrick Massot]

And of course it has nothing to do with ultrafilters so you should put in the basic filter file defining comap as

lemma filter.comap_ne_bot_of_image_mem {F : filter Y} [ne_bot F] {f : X → Y} {A : set X}
  (h : f '' A ∈ F) :  (comap f F).ne_bot :=
begin
  apply comap_ne_bot (λ U U_in, _),
  rcases (filter.nonempty_of_mem $ inter_mem h U_in) with ⟨-, ⟨x, -, rfl⟩, h⟩,
  exact ⟨x, h⟩
end

[Patrick Massot]

And then, having reached this state, you'll realize it's already there.

[Bernd Losert]

Aha. Nice find. There's so many of this little lemmas, I get lost trying to find what I need, especially when I have to jump between the filter and ultrafilter stuff.

[Bernd Losert]

I'm trying to use it in this bigger lemma, but it doesn't work:

import tactic
import order.filter.partial
import order.filter.ultrafilter
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 ℱ := comap f 𝒱,
  haveI : ℱ.ne_bot := filter.comap_ne_bot_of_image_mem 𝒱.ne_bot h,
  let 𝒰 := ultrafilter.of ℱ,
  use 𝒰,
  have h : 𝒰.map f = 𝒱, sorry,
  have h' : A ∈ 𝒰, sorry,
  exact and.intro h h',
end

[Bernd Losert]

unknown identifier 'filter.comap_ne_bot_of_image_mem' is the error.

[Bernd Losert]

Oops. It's called filter.ne_bot.comap_of_image_mem. Haha.