How to solve m * (m - 1) + m * 2 = m + m ^ 2 for Nat

Stream: new members

[Heliopolis]

I had trouble with solving m * (m - 1) + m * 2 = m + m ^ 2 where m is a natural number. 'omega' cannot easily do it. Here is my solution and I believe it is unnecessarily long:

import Mathlib

example (m : ℕ) : m * (m - 1) + m * 2 = m + m ^ 2 := by

  -- discuss m = 0 and m ≠ 0

  by_cases h : m = 0

  . -- when m = 0 its trivial

    rw [h]

    norm_num

  . -- when m ≠ 0

    replace h : m ≠ 0 := by omega

    -- prove it by calculation

    calc m * (m - 1) + m * 2 = m * (m - 1) + m + m := by omega

      _ = m * (m - 1 + 1) + m := by linarith

      _ = m * m + m := by rw [Nat.sub_one_add_one h] -- m - 1 + 1 = m

      _ = m + m ^ 2 := by ring

Could somebody help me with it? How to solve it simpler? Thanks a lot!

[Markus Himmel]

Here is a proof that is similar to yours but slightly shorter:

import Mathlib

example {m : Nat} : m * (m - 1) + m * 2 = m + m ^ 2 :=
  match m with
  | 0 => by simp
  | m + 1 => by
    simp only [add_tsub_cancel_right]
    ring

[Riccardo Brasca]

@Heliopolis there are surely various ways of golfing it (ie making it shorter), but my suggestion is in general to avoid natural subtraction, at least if you are a beginner.

[Heliopolis]

@Markus Himmel Thanks a lot!