Zulip Chat Archive

Stream: new members

Topic: congr under an existential


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Sep 21 2020 at 22:17):

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

view this post on Zulip Yakov Pechersky (Sep 21 2020 at 22:20):

Ah, a variant of exists.imp

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 22:38):

Oh, it's the elab order

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 21 2020 at 22:39):

What are you trying to do?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 22:42):

but you did that

view this post on Zulip Mario Carneiro (Sep 21 2020 at 22:42):

so that must not be the problem

view this post on Zulip Yakov Pechersky (Sep 21 2020 at 22:42):

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

view this post on Zulip 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