rw [← add_smul] fails to find pattern in Vector Space World

Stream: new members

[Stephen Thoemmes]

Hi everyone,
(I am totally new to Lean and trying to brush up on Linear Algebra)

I'm working through the Linear Algebra "Vector Space World" Lean game (Level 1/5: zero scalar multiplication), and I'm stuck on what seems like a type inference issue with rewrite.

Goal: Prove zero_smul_v: that (0 : K) • w = (0 : V) in a vector space.
Setup: After applying add_right_cancel (b := 0 • w), my goal becomes:

w: V
⊢ 0 • w + 0 • w = 0 • w

Problem: I want to rewrite 0 • w + 0 • w to (0 + 0) • w using add_smul backwards. The theorem add_smul has signature:

{R} {M} [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x : M) : (r + s) • x = r • x + s • x

But rw [← add_smul] fails with:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?r • ?x + ?s • ?x

What I've tried:

• rw [← add_smul]
• rw [← add_smul 0 0 w]
• rw [← add_smul (0 : K) (0 : K) w]
• rw [← @add_smul K V _ _ _ 0 0 w]

All give the same error. The pattern 0 • w + 0 • w is literally in the goal, so I'm confused why Lean can't find it.

The game doesn't have access to conv, simp, change, or linarith.

Any ideas what's going on or how to work around this?

Thanks!

[Stephen Thoemmes]

Please let me know if I should ask this in another channel instead

[Snir Broshi]

Hello :wave:
Such questions should be asked in #new members, but do not post a duplicate there; an admin will probably move this thread to there soon

[Snir Broshi]

As for your question, when rw fails with such an error where it looks obvious that the pattern is in the goal, I find it helps to hover over stuff to check their type, in both your goal and the question mark thingies (metavariables) in the error message

[Snir Broshi]

Here you'll find that your goal has two different zeros. One is of type K, and the other is a natural number

[Snir Broshi]

You introduced natural number zero with the first apply, so the solution is to do:
apply add_right_cancel (b := (0 : K) • w)

[Snir Broshi]

Just found out that this is what the game itself recommends when you press "Show more help" on that level.
Did they introduce you to similar casting issues before? If not, then I highly recommend watching this Lean Real-Analysis course, I think it's a nice beginner-friendly introduction to Lean.

[Stephen Thoemmes]

This is amazing info, thank you so much.

[Notification Bot]

This topic was moved here from #lean4 > rw [← add_smul] fails to find pattern in Vector Space World by Patrick Massot.