Mechanics of Proof 1.3.11 ex 10

Stream: lean4

[rzeta0]

I am a newbie to both maths and lean. I am working through the Mechanics of Proof book, and have done all the exercises in the first section 1.3 (I did need a hint with ex 15) - except this one exercise 10.

Following the examples, the standard pattern seems to be to "introduce" terms which are amenable to substitution using a hypothesis. Indeed this has worked well for other exercises.

Note - we are only using rw and ring at this point in the book.

This is where it gets me:

example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 :=
    calc
      p = (5*p - 3) - 4*p + 3 := by ring
      _ = (3*p + 1) - 4*p + 3 := by rw [h1]
      _ = -p + 4 := by ring

I can't find a way to get rid of the p on the RHS. Other combinations that I've tried end up with a larger multiple of p on the RHS.

I also notice that the hypothesis reduces 5p down to 3p, which suggests it can be done again down to 1p. But I have failed to find a way to do so.

[Antoine Chambert-Loir]

I would start from writing p = - (5 * p - 3) + … and then rw [h1].
(The mathematical idea is toguess what multiple of $5p-3$, once replaced by $3p+1$, will cancel the peas.)

[rzeta0]

thanks Antoine - actually it seems +(5*p -3) was the right starting point:

example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 :=
    calc
      p = (5*p - 3)/2 - (3*p - 3)/2 := by ring
      _ = (3*p + 1)/2 - (3*p - 3)/2 := by rw [h1]
      _ = 2 := by ring

If anyone is interested, I eventually used the following method to work out which multiples I needed:

$$a*5 +b = 1 \\ \\ a*3 +b = 0$$

which gives, $a=1/2$ and $b=-3/2$

[Kevin Buzzard]

Probably the illegal-in-this-context polyrith tactic just solves the goal immediately?