turn a + b = a into something like a + b = a + 0

Stream: new members

[AnduinHS]

Hello everyone!
Induction will work. Howver, I want to turn a + b = a into something like a + b = a + 0. There are two attempts
360截图18750810102140132.png

1. add_zero is defined for mynat, i.e. a + 0 = a. And here I am told that rw (rewrite) in lean can replace X in goal or hypothesis (add at h after it, h is hypothesis) with the equivalent Y, and rw <- replaces Y with the equivalent X. Here I am trying to replace a with a + 0 (i.e. add_zero backwards, but it doesn't seem to work (I don't know if it's possible to specify the element you want to replace in lean)
2. 360截图17860605423034.png
   Why couldn't I use my lemma ex above to replace "a" or lean auto-detected other elements with "a+0"? What are "metavariables"?
   

Thank you in advance!

[Ruben Van de Velde]

In the NNG, you can do rw ←add_zero a, though that doesn't fix everything - it replaces every a by a + 0.
This works, but I'm not sure you learned about conv yet:

intro h,
conv at h { to_rhs, rw ←add_zero a } ,
exact add_left_cancel _ _ _ h,

[Damiano Testa]

I see that Ruben already answered this!

[Eric Rodriguez]

We're not taught conv in the NNG at all, and in fact I just looked up my proof for that propn -- it's really ugly. I think some note about either conv or nth_rewrite at that point, because it feels like the thing you'd do if you were proving this by hand.

[Bryan Gin-ge Chen]

For what it's worth, you don't need conv or nth_rewrite for this proof. See the "official" solution here.

[Ruben Van de Velde]

The "issue" here is that lean finds it easier to simplify expressions than to complicate them - so it's easier to do the apply first, and then remove the + 0, than to add + 0 first to get your hypothesis in the right shape

[Ruben Van de Velde]

And if you're into that, you can do it in one line without tactics:

lemma eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0 := λ h, add_left_cancel _ _ _ (h.trans (add_zero _).symm)

[Eric Rodriguez]

Ruben Van de Velde said:

The "issue" here is that lean finds it easier to simplify expressions than to complicate them - so it's easier to do the apply first, and then remove the + 0, than to add + 0 first to get your hypothesis in the right shape

I feel like having read this line (or something similar) whilst doing the proof would've been really helpful to me, bach when I was getting started. I may PR some text to this effect later