Mathematics in Lean section 2.5

Stream: new members

[Yoni Katzuv]

Hello,
I'm working through Mathematics in Lean and I've reached the final exercise in Chapter 2:

variables {X : Type*} [metric_space X]
variables x y z : X

example (x y : X) : 0 ≤ dist x y := sorry

The book recommends using the theorem nonneg_of_mul_nonneg_left.
However, I cannot find a way to apply it without having to make its implicit arguments explicit:

#check @nonneg_of_mul_nonneg_left _ _ 2 (dist x y)

works but

#check (nonneg_of_mul_nonneg_left : 0 ≤ 2 * dist x y → 0 < 2 → 0 ≤ dist x y)

gives

invalid type ascription, term has type
  0 ≤ ?m_3 * ?m_4 → 0 < ?m_3 → 0 ≤ ?m_4
but is expected to have type
  0 ≤ 2 * dist x y → 0 < 2 → 0 ≤ dist x y

Is this case just too hard for type inference or am I missing something?