A theorem about polynomial parametrizations

Stream: new members

[Burak Yıldız]

I have verified by pen and paper the following theorem given below. However, Lean 4 said "tactic 'rfl' failed". I also used just ring tactic and it suggested using ring_nf instead but this time said "unsolved goals". That would be great if someone could help me in proving this correctly.

import Mathlib.Tactic
import Mathlib.Algebra.Polynomial.Basic
set_option maxHeartbeats 5000000

noncomputable def X : Polynomial ℤ := Polynomial.X
noncomputable def x₁ : Polynomial ℤ := 4 * X ^ 2 - 25 * X + 36
noncomputable def x₂ : Polynomial ℤ := 8 * X ^ 2 - 50 * X + 74
noncomputable def x₃ : Polynomial ℤ := 4 * X - 16
noncomputable def x₄ : Polynomial ℤ := 4 * X - 12
noncomputable def y : Polynomial ℤ :=(2) * (2)* (4)* (4 * X - 11) * (2 * X - 7)*(2 * X - 5) * (4 * X - 15) * (4 * X - 9) * (X - 4) * (4 * X - 13) * (X - 3) * (4 * X^2 - 25 * X + 37) *(4 * X^2 - 25 * X + 38)

theorem totalProduct_is_square :
x₁ * (x₁+1) * (x₁+2) * (x₁+3) * x₂ * (x₂+1) * (x₂+2) * (x₂+3) * x₃ * (x₃+1) * (x₃+2) * (x₃+3) * x₄* (x₄+1) * (x₄+2) * (x₄+3)= y * y := by
ring_nf
rfl

[Jz Pan]

Maybe before ring you need simp only [X, x₁, x₂, x₃, x₄, y]

[Jz Pan]

Otherwise they will not get expanded

[Burak Yıldız]

Thanks very much, it works.