## Stream: general

### Topic: rw using an iff

#### Bernd Losert (Jan 09 2022 at 19:21):

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

#### Kyle Miller (Jan 09 2022 at 19:22):

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

#### Bernd Losert (Jan 09 2022 at 19:24):

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 (Jan 09 2022 at 19:25):

Rewrite it in the other direction:

rw โfilter.forall_mem_nonempty_iff_ne_bot


#### Bernd Losert (Jan 09 2022 at 19:27):

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

#### Bernd Losert (Jan 09 2022 at 19:31):

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 (Jan 09 2022 at 19:34):

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

#### Bernd Losert (Jan 09 2022 at 19:41):

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 (Jan 09 2022 at 19:52):

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

#### Kyle Miller (Jan 09 2022 at 19:57):

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 (Jan 09 2022 at 19:58):

Doesn't the a in A work?

#### Patrick Massot (Jan 09 2022 at 19:59):

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 (Jan 09 2022 at 20:08): 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 (Jan 09 2022 at 20:11):

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 (Jan 09 2022 at 20:12):

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

#### Bernd Losert (Jan 09 2022 at 20:21):

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 (Jan 09 2022 at 20:30):

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 (Jan 09 2022 at 20:32):

unknown identifier 'filter.comap_ne_bot_of_image_mem' is the error.

#### Bernd Losert (Jan 09 2022 at 20:35):

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

Last updated: Aug 03 2023 at 10:10 UTC