neg_eq_neg_one_mul

Stream: new members

[Vasily Ilin]

why does

... = (a*a + b*a) - b*a - b*b : by {rw ← sub_sub}
... = a*a + b*a + (-1)*b*a - b*b : by {rw neg_eq_neg_one_mul (b*a)}

fail? The error is "rewrite tactic failed, did not find instance of the pattern in the target expression -(b * a)"

[Rémy Degenne]

I guess that's because sub and neg are not the same thing. The - sign that you have before b*a in your expression is subtraction, not negation. You can use sub_eq_add_neg to transform x - y into x + - y (which is changing sub into add and neg).

It would be easier to help you if you posted a #mwe

[Vasily Ilin]

That was exactly the issue. Thank you!