equality on filters to eq. on ultrafilters

Stream: general

[Bernd Losert]

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*}

example (f : X → Y) (𝒰 : ultrafilter X) (𝒱 : ultrafilter Y) (h : map f 𝒰 = 𝒱) : 𝒰.map f = 𝒱 := ???

I'm having trouble doing this example. I know that I need to useultrafilter.of_coe and ultrafilter.of_coe somehow, but I always get stuck.

[Patrick Johnson]

example (f : X → Y) (𝒰 : ultrafilter X) (𝒱 : ultrafilter Y) (h : map f 𝒰 = 𝒱) : 𝒰.map f = 𝒱 :=
by rw [ultrafilter.map, ultrafilter.of_compl_not_mem_iff]; cases 𝒱; congr; exact h

[Patrick Massot]

example (f : X → Y) (𝒰 : ultrafilter X) (𝒱 : ultrafilter Y) (h : map f 𝒰 = 𝒱) : 𝒰.map f = 𝒱 :=
by exact_mod_cast h

[Patrick Massot]

That's exactly the job of tactic#norm_cast and its cousins

[Bernd Losert]

Wow, what a nice tactic. Thanks.

[Bernd Losert]

Hmm... I'm getting an error when I try to use it.

[Bernd Losert]

Here's my 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
  -- 𝒰 will be the ultrafilter generated by the filter base { (f ⁻¹' V ∩ A) | V ∈ 𝒱 }
  let B₀ : set X := f⁻¹' (f '' A) ∩ A,
  let ℬ : filter_basis X := {
    sets := { (f ⁻¹' V ∩ A) | V ∈ 𝒱 },
    nonempty := ⟨B₀, f '' A, h, rfl⟩,
    inter_sets := begin
      assume B : set X,
      assume B' : set X,
      rintro ⟨V : set Y, h₁ : V ∈ 𝒱, h₂ : f ⁻¹' V ∩ A = B⟩,
      rintro ⟨V' : set Y, h₁' : V' ∈ 𝒱, h₂' : f ⁻¹' V' ∩ A = B'⟩,
      let B'' := B ∩ B',
      use B'',
      split,
      have h' : f ⁻¹' (V ∩ V') ∩ A = B'', from calc
        f ⁻¹' (V ∩ V') ∩ A = (f ⁻¹' V ∩ f ⁻¹' V') ∩ A : by rw set.preimage_inter
        ... = (f ⁻¹' V ∩ A) ∩ (f ⁻¹' V' ∩ A) : by {ext, simp, tauto}
        ... = B ∩ B' : by rw [h₂, h₂'],
      exact ⟨V ∩ V', 𝒱.inter_sets h₁ h₁', h'⟩,
      simp [set.subset.rfl],
    end,
  },
  let ℱ := ℬ.filter,
  have : A ∈ ℱ := ℬ.mem_filter_iff.mpr ⟨B₀, ⟨f '' A, h, rfl⟩, set.inter_subset_right (f⁻¹' (f '' A)) A⟩,
  haveI : ℱ.ne_bot := sorry,
  let 𝒰 := ultrafilter.of ℱ,
  use 𝒰,
  split,

  show 𝒰.map f = 𝒱, begin
    have : ∀ (V : set Y), V ∈ 𝒱 → f ⁻¹' V ∈ ℱ, begin
      assume V : set Y,
      assume hV : V ∈ 𝒱,
      rw filter_basis.mem_filter_iff ℬ,
      let B := f ⁻¹' V ∩ A,
      use B,
      split,
      show B ∈ ℬ, from ⟨V, hV, rfl⟩,
      show B ⊆ f ⁻¹' V, from set.inter_subset_left (f ⁻¹' V) A,
    end,
    have : map f 𝒰 ≤ 𝒱, from calc
      map f 𝒰 ≤ map f ℱ : filter.map_mono (ultrafilter.of_le ℱ)
      ... ≤ 𝒱 : by exact (filter.tendsto_def.mpr this),
    have : map f 𝒰 = 𝒱, from (𝒱.unique this),
    exact_mode_cast this, -- HERE IS WHERE IT FAILS
  end,

  show A ∈ 𝒰, sorry,
end

[Floris van Doorn]

you misspelled the tactic ;-)

[Bernd Losert]

In what way? exact_mode_castis a tactic and I am in tactic mode.

[Alex J. Best]

its exact mod cast

[Bernd Losert]

Hmm... how did that e get in there. Haha.

[EDY SAUL CONDORHUANCA RIMACHI]

Hi. I have this problem to install. AFTER WRITE THIS echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile. APPEAR THIS ERROR bash: $HOME/.profile.: ambiguous redirect
How to fix?

[Patrick Johnson]

@EDY SAUL CONDORHUANCA RIMACHI Please ask your question in a new topic.