Unexpected meta goals

Stream: new members

[Vasily Ilin]

Why does the below generate meta goals?

import data.polynomial
open polynomial
variables {R : Type} [comm_ring R]

example (n : ℕ) : (n + X.nat_degree ≤ n + 1) :=
begin
  have : X.nat_degree ≤ 1,
  -- have 4 goals now!
end

[Ruben Van de Velde]

It doesn't realise what X's base ring is

[Ruben Van de Velde]

So have : (X : R[X]).nat_degree..., or just continue and see if lean can figure them out on its own

[Damiano Testa]

Also, looking at the code that you posted, I would guess that you intended the X in the statement to be in R[X], but I think that Lean guesses ℕ[X].

(All this is very speculative, of course.)