congr under an existential

Stream: new members

[Yakov Pechersky]

Is there an existing lemma that says the following? Is it a pi lemma?

example {α β γ δ : Type} {x y : α} {f : α → β → γ} {g : γ → δ} (h : ∃ z, f x z = f y z) :
  ∃ z, g (f x z) = g (f y z) :=
begin
  obtain ⟨z, hz⟩ := h,
  use z,
  rw hz,
end

[Yakov Pechersky]

I guess the reverse, with a hypothesis about injectivity of g is what I really want.

[Yakov Pechersky]

Ah, a variant of exists.imp

[Yakov Pechersky]

So, why does the first example work but not the second?

lemma exists_inj {α β γ δ : Type} {x : α} {f : α → β} {g : β → γ} (hg : function.injective g)
  (h : ∃ z, g (f x) = g z) : ∃ z, f x = z :=
Exists.imp (λ z H, @hg (f x) z H) h

lemma exists_inj {α β γ δ : Type} {x : α} {f : α → β} {g : β → γ} (hg : function.injective g)
  (h : ∃ z, g (f x) = g z) : ∃ z, f x = z :=
Exists.imp (λ z H, hg H) h

[Mario Carneiro]

function.injective is a definition that wraps something like \forall {{x y}}, f x = f y -> x = y

[Yakov Pechersky]

So it can't infer the (f x) or z. Got it. In any case, this isn't leading me down to where I want because of the "exists can only elim into prop" issue.

[Mario Carneiro]

Oh, it's the elab order

[Mario Carneiro]

lemma exists_inj {α β γ δ : Type} {x : α} {f : α → β} {g : β → γ} (hg : function.injective g)
  (h : ∃ z, g (f x) = g z) : ∃ z, f x = z :=
h.imp (λ z H, hg H)

this works fine

[Mario Carneiro]

What are you trying to do?

[Yakov Pechersky]

I'm basically trying to do the equivalent of an apply_fun on both sides of an equality that is behind an existential.

[Mario Carneiro]

but you did that

[Mario Carneiro]

so that must not be the problem

[Yakov Pechersky]

I'm going to try something, will be back later with attempts.

[Mario Carneiro]

Generally, you should open an existential if you want to work on the contents