How to solve simple algebra problems

Stream: new members

[Jayson Amati]

What is the general way of solving simple algebra problems?
Such as the following:

theorem n_is_620  (m n : ℚ) (h : ((3 / 4) * m) * (n - 120) = m * (n - 245))  :  n = 620 := by
  sorry

[Daniel Weber]

I think polyrith should be able to handle this

[Daniel Weber]

Actually, this isn't true — m could be 0

[Daniel Weber]

If you add the assumption it isn't you can use linear_combination with 1/m, I think

[Rida Hamadani]

And if you simplify it a bit linarith can do it too, this is some horrible code but it does the job:

import Mathlib

theorem n_is_620  (m n : ℚ)
    (h : ((3 / 4) * m) * (n - 120) = m * (n - 245)) (hm : m ≠ 0)  :  n = 620 := by
  have h' : ((3 / 4) * m) * (n - 120) * (1 / m) = m * (n - 245) * (1 / m) := by simp [h]
  ring_nf at h'
  simp [mul_comm m n,hm] at h'
  linarith

[Jayson Amati]

Yeah

Daniel Weber said:

Actually, this isn't true — m could be 0

Yeah you are right, that should be an assumption.

[Jayson Amati]

Daniel Weber said:

If you add the assumption it isn't you can use linear_combination with 1/m, I think

I'll try this . Thank you for the suggestion.

[Jayson Amati]

Rida Hamadani said:

And if you simplify it a bit linarith can do it too, this is some horrible code but it does the job:

import Mathlib

theorem n_is_620  (m n : ℚ)
    (h : ((3 / 4) * m) * (n - 120) = m * (n - 245)) (hm : m ≠ 0)  :  n = 620 := by
  have h' : ((3 / 4) * m) * (n - 120) * (1 / m) = m * (n - 245) * (1 / m) := by simp [h]
  ring_nf at h'
  simp [mul_comm m n,hm] at h'
  linarith

Oh nice!
So what I'm getting from this is that if the expressions are simple enough linarith or polyrith will generally solve such problems.
The "trick" is in simplifying them enough?

[Jayson Amati]

Thanks @Rida Hamadani .

[Rida Hamadani]

Yes exactly, in general your thought process should be "how can I simplify this enough so that the automation can handle it on its own?", and usually this involves steps that are hard to automate, like multiplying both sides by a specific term (in this case 1/m, which I did in the have, but there are better ways to do it).

[Jayson Amati]

What would be the better ways? More automation at the beginning of the simplification? Or using different tactics? Or something else ?

[Rida Hamadani]

I just think it is not tidy, maybe it would be cleaner if I used a lemma instead of the have and if I avoided the non-terminal simp, but this is just a personal preference here.