Why doesn't `?m_2 ≠ 0` unify with `2 ≠ 0`?

Stream: new members

[Martin C. Martin]

Why does the following give me an error?

import data.nat.gcd

example {k n : ℕ}  (h : 2 * (2 * k^2) = 2 * n^2) : 2 * k^2 = n^2 :=
begin
  exact (mul_right_inj' two_ne_zero).mp h
end

Shouldn't it be able to deduce that the type is nat? Or is there something else going wrong?

[Ruben Van de Velde]

Does the proof go through if you help it along, like with @two_ne_zero \N _ _ _ (for some number of underscores)?

[Martin C. Martin]

Yes it does, thanks for the tip! I thought the problem was in mul_right_inj', but I see it's in two_ne_zero.

[Ruben Van de Velde]

I think the problem is that both of those lemmas are generic, so lean finds it hard to figure out their types simultaneously