tactic 'introN' failed, insufficient number of binders

Stream: new members

[Sam Vervaeck]

Hi all, I'm a total beginner when it comes to Lean (and to be honest mathematics) and I'm doing the Natural Numbers Game to learn more. I'm stuck at this exercise:

theorem succ_le_succ (x y : ℕ) (hx : succ x ≤ succ y) : x ≤ y := by
  intro h

I get the following error:

Line 1, Character 0

tactic 'introN' failed, insufficient number of binders
xy: ℕ
hx: succ x ≤ succ y
⊢ x ≤ y

I've looked at sample solutions and at least one starts with this. Is this some kind of bug in the Natural Numbers Game server? If not, do I need to use something else like induction?

By the way if anyone has any hints on what resources to read, I'm all ears :)

All the best,
Sam

[Etienne Marion]

Hi, and welcome! The intro tactic is supposed to be used on a goal of the form p -> q, to introduce the hypothesis p. But here your hypotheses are already introduced (they are x, y and hx), so intro has nothing to introduce.

[Sam Vervaeck]

Wow that I missed that! Thanks!