# Zulip Chat Archive

## 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.

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

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