Metavariables?

Stream: new members

[Kristaps John Balodis]

I have 3 related questions about metavariables, but allow me to set the stage, so you know where I'm coming from.
I'm trying to do Level 1/4 of Advanced Multiplication World from The Natural Number Game, which is asking to prove

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=

So far, I've come up with

begin
intro a_zero,
intro b_zero,
cases b,
rw mul_zero,
apply b_zero,

intro h,
rw mul_succ at h,

sorry
end

which leaves me with a goal state of

case mynat.succ
a : mynat,
a_zero : a ≠ 0,
b : mynat,
b_zero : succ b ≠ 0,
h : a * b + a = 0
⊢ false

Now one thing I'm trying at this point, is to force a to be zero, however when I try writing

rw eq_zero_of_add_right_eq_self at h,

Lean is telling me it won't apply the tactic because the lhs is a "metavariable".
1) What is a metavariable?
2) Why can't I use this tactic on metavariables?
3) How should I proceed?

[Thomas Browning]

The lemma eq_zero_of_add_right_eq_self is an implication. You can only use rw with equalities and iffs

[Thomas Browning]

Also, I think that you want to use add_left_eq_zero rather than eq_zero_of_add_right_eq_self

[Kristaps John Balodis]

That seems to give me the same error about metavariables, as does add_right_eq_zero

[Thomas Browning]

You can't use rw with add_right_eq_zero, since it is an implication

[Thomas Browning]

Instead, maybe start with have key := add_right_eq_zero h

[Thomas Browning]

That directly feeds h into add_right_eq_zero

[Kristaps John Balodis]

That seemed to work. The only issue is, have key has not been introduced in The Natural Number Game yet, so there ought to be some other way of making this work.

[Kristaps John Balodis]

Ah, but have has been introduced, and that seems to work without writing key , thanks!

[Alex J. Best]

key is just an optional name you can give the hypothesis, if you don't give a name have will call it this by default which becomes annoying if you have more than one thing, they end up all called this!

[Kyle Miller]

@Kristaps John Balodis Roughly speaking, a metavariable is what Lean uses to fill in missing details automatically, and Lean solves for metavariables in a process called unification. I think what's happening here is that it wasn't sure what b was supposed to be.