How to multiply both sides of the goal by 3

Stream: new members

[Zihao Zhang]

import Mathlib

example {n:Nat}:n * (2 * n - 1) * (2 * n + 1) / 3 + (2 * (n + 1) - 1) * (2 * (n + 1) - 1) =
  (n + 1) * (2 * (n + 1) - 1) * (2 * (n + 1) + 1) / 3:=by
  sorry

I want to multiply the right side of both expressions in the goal by 3.

[Michael Rothgang]

Be careful: your goal probably doesn't say you think it does, because it uses subtraction and division of natural numbers. (In the natural numbers, you have 2 - 3 = 0 and 5 / 2 = 2, for example.) This makes your goal much harder to prove.

[Michael Rothgang]

The first fix is to use e.g. rational numbers, as in

import Mathlib

example {n: ℚ} : n * (2 * n - 1) * (2 * n + 1) / 3 + (2 * (n + 1) - 1) * (2 * (n + 1) - 1) =
  (n + 1) * (2 * (n + 1) - 1) * (2 * (n + 1) + 1) / 3 := by
  sorry

[Michael Rothgang]

(Style side note: in mathlib, we prefer putting spaces around the colon also, like I did above.)

[Michael Rothgang]

If you're allowed to use powerful tactics now, you can use e.g. field_simp (which cancels the division and does a few more simplifications) or ring (which solves your goal altogether).

[Zihao Zhang]

I understand that in the natural numbers, 2–3 is defined to be 0, and I’ve verified that this example is correct.

[Michael Rothgang]

Do you have a particular reason to use natural numbers here?

[Zihao Zhang]

This is required for a sub-goal within a more intricate proof.

[Zihao Zhang]

I’d like to know if there’s a simple way to multiply by 3 on the right, instead of using have.

[Zihao Zhang]

have h1:3 ≠ 0:=by simp
  rw [←Nat.mul_left_inj h1]

I found one, though it used have.

[Yongxi Lin (Aaron)]

Try rw [← Nat.mul_left_inj (by simp : 3 ≠ 0)] if you really disliked the have tactic

[Zihao Zhang]

@Yongxi Lin (Aaron) Thank you! It is perfect.

[Ruben Van de Velde]

We probably have docs#three_ne_zero as a lemma

[Alfredo Moreira-Rosa]

More generally, when you want to apply the same function to both sides of an equation, you can use apply_fun . It will create a second sub goal to prove the function you are applying is injective.