[thaumasiotes]

> @GP?: Doesn't Lean have a "please fill the blanks" mode for short proof?

Yes, there are several depending on what you want to do. The catchall is `simp` (short for 'simplify').

Why do we need more than one "do what I mean" command? (Or more than zero "do what I say" commands?) Because it's impossible to know what you mean. If you try to use a lot of `simp`, you'll notice that you often have to tell it what to do.

Note that what we really want for this problem is a linear algebra package that can do row reduction, not a formal prover. This problem is all arithmetic.