CoCalc injectivity

Stream: general

[Emiel Lanckriet]

I made the exercise about injectivity of compositions in CoCalc, first I tried:

intros a b,
intro hab,
apply hg,

But got the error:

invalid apply tactic, failed to unify
  a = b
with
  ?m_1 = ?m_2
state:
X Y Z : Type,
f : X → Y,
hf : injective f,
g : Y → Z,
hg : injective g,
a b : X,
hab : (g ∘ f) a = (g ∘ f) b
⊢ a = b

Could someone tell why a=b cannot unify with ?m_1 = ?m_2.
I know this is wrong and the correct answer is first apply hf, but I just want to know why it doesn't unify.

[Kevin Buzzard]

``` not ´´´ (the one at the top)

[Kevin Buzzard]

It can't unify it because the conclusion of hg is that two terms of type Y are equal, but a and b have type X.

[Patrick Massot]

(deleted)

[Emiel Lanckriet]

Ah, ok, thanks, I hadn't thought that far. Thanks a lot.