## Stream: new members

### Topic: congr under an existential

#### Yakov Pechersky (Sep 21 2020 at 22:03):

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 (Sep 21 2020 at 22:17):

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

#### Yakov Pechersky (Sep 21 2020 at 22:20):

Ah, a variant of exists.imp

#### Yakov Pechersky (Sep 21 2020 at 22:27):

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 (Sep 21 2020 at 22:37):

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

#### Yakov Pechersky (Sep 21 2020 at 22:38):

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 (Sep 21 2020 at 22:38):

Oh, it's the elab order

#### Mario Carneiro (Sep 21 2020 at 22:38):

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 (Sep 21 2020 at 22:39):

What are you trying to do?

#### Yakov Pechersky (Sep 21 2020 at 22:40):

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

but you did that

#### Mario Carneiro (Sep 21 2020 at 22:42):

so that must not be the problem

#### Yakov Pechersky (Sep 21 2020 at 22:42):

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

#### Mario Carneiro (Sep 21 2020 at 22:43):

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

Last updated: May 11 2021 at 22:14 UTC