Prove problem

Stream: new members

[lexuan]

In Lean4, how to prove that -↑n1 - ↑n1 * ↑n2 = -↑(n1 + n1 * n2 - 1) - 1

[Asei Inoue]

try omega

[lexuan]

Thank you, this nicely solves the goal.

[Notification Bot]

This topic was moved here from #lean4 > Prove problem by Yury G. Kudryashov.

[Yury G. Kudryashov]

@lexuan I moved your question here. Next time please post a #mwe E.g., one has to guess what types are involved in the formula you've posted.

[lexuan]

"Understood, the types in Lean 4 are very crucial, and I will pay attention next time."