easy inductive proof - noob to syntax

Stream: general

[Quinn]

inductive even : ℕ → Prop :=
| even_zero : even 0
| even_add_two : ∀ n, even n → even (n + 2)

theorem even_property (n : ℕ) (h : even n) : ∃ k, n = 2 * k :=
begin
    induction h with n h IH.
    { use 0, simp, },
    { cases ih with k hk, use k + 1, simp only [hk], linarith, }.
end

I know this proof in coq, but in lean my error message is

[0/6] Building LeanDelendum.Basic
error: > LEAN_PATH=./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /nix/store/mrb3i1b78iysik1lhsij5jdihjyja59n-lean4-4.5.0/bin/lean ./././LeanDelendum/Basic.lean -R ././. -o ./.lake/build/lib/LeanDelendum/Basic.olean -i ./.lake/build/lib/LeanDelendum/Basic.ilean -c ./.lake/build/ir/LeanDelendum/Basic.c
error: stdout:
./././LeanDelendum/Basic.lean:5:54: error: typeclass instance problem is stuck, it is often due to metavariables
  HMul Nat ?m.344 ℕ
./././LeanDelendum/Basic.lean:7:16: error: unexpected token 'with'; expected command
./././LeanDelendum/Basic.lean:10:0: error: invalid 'end', insufficient scopes

[Quinn]

i don't see the typeclasses, is the inductive a typeclass under the hood? that would be the reverse of coq, haha

[Quinn]

also what's a metavariable, in this context?

[Julian Berman]

That looks like Lean 3 syntax, which is dead.

[Julian Berman]

(And your error message is indeed saying you're using Lean 4)

[Quinn]

excellent.

[Quinn]

Thank you.

[Quinn]

what is "declaration has free variable"? the variable is clearly bounded!

inductive Even : ℕ → Prop :=
| even_zero : Even 0
| even_add_two (n : ℕ) : Even n → Even (n + 2)

[Quinn]

oh am i naive to assume 0 and 2 literals will fly with \N?

[Shreyas Srinivas]

This works:

import Mathlib.Tactic

namespace Playground

  inductive Even : ℕ → Prop where
    | even_zero : Even 0
    | even_add_two (n : ℕ) : Even n → Even (n + 2)

end Playground

[Shreyas Srinivas]

The abbreviation ℕ doesn't represent Natural Numbers outside Mathlib if I recall correctly.

[Kyle Miller]

Indeed, it's defined in Mathlib.Init.Data.Nat.Notation