Injective under exists

Stream: new members

[Yakov Pechersky]

Is there the equivalent of this statement, that one can apply an injective function under an existential? Maybe somewhere in pi?

example {α β γ : Type*} {y : β} {f : α → β} {g : β → γ} (g_inj : function.injective g)
  (h : ∃ x, g (f x) = g y) : ∃ x, f x = y :=
exists.elim h (λ x H, exists.intro x (g_inj H))

[Mario Carneiro]

That looks like exists.imp g_inj

[Mario Carneiro]

example {α β γ : Type*} {y : β} {f : α → β} {g : β → γ} (g_inj : function.injective g)
  (h : ∃ x, g (f x) = g y) : ∃ x, f x = y := h.imp (λ _ H, g_inj H)

[Yakov Pechersky]

Great, thanks!