Best way to render "simplify both sides of an equation."

Stream: new members

[Martin C. Martin]

When trying to prove a = b, you might establish c = d, then subtract e from both sides and simplify, giving the goal. What’s the standard way to represent that in Lean? You could use calc mode to turn a into c - e, and then the rest is straight forward, but that first step of “de-simplifying” seems unnatural and unmotivated. Is that the accepted method?

In Linear Algebra Done Right, the proof that 0 • v = 0 starts with 0 • v = 0 • v + 0 • v , then subtracts 0 • v from both sides and simplifies. I could start with 0 = 0 • v - 0 • v, but that seems unnatural & unmotivated.

[Yaël Dillies]

Does

suffices h : your_statement,
{ simpa using h }

do what you want?

[Kyle Miller]

For these little proofs, I've written things like 0 = 0 • v - 0 • v = (0 + 0) • v - 0 • v = 0 • v + 0 • v - 0 • v = 0 • v on the blackboard. I like it because it's a little exercise in getting used to pulling a 0 + 0 = 0 out of nowhere because it'll be justified by what comes later, and also I like it because purely equational reasoning has a certain charm.

[Kyle Miller]

Yaël's suggestion is a good tool for putting things into a logical order. You can also try getting comfortable with different congr lemmas, which might help here. There are also the convert and convert_to tactics, which you can use to generate sub-goals when things don't match up completely; however calc usually gives clearer proofs.

[Martin C. Martin]

Thanks to both of you!

[Anatole Dedecker]

It’s not used a lot in mathlib, but you may also be interested by tactic#apply_fun