Equivalence of algebraic identities

Stream: general

[Heather Macbeth]

Is there a fully automated (i.e., tactics only) way of doing this:

import data.real.basic

example (a : ℝ) :
  a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1
  ↔ a * (a ^ 2 - 1 / 2) * (4 * a ^ 3 - 3 * a) = 0 :=
sorry

The most progress I could make was

begin
  have : 0 ≠ 2 := by norm_num,
  ring,
  field_simp [this],
  ring,

end

(both rings are necessary) but this only reduces it to the goal

(16 * a ^ 2 - 20) * a ^ 2 + 6 = 0 ∨ a ^ 2 = 0 ↔ (8 * a ^ 2 - 10) * a ^ 2 + 3 = 0 ∨ a ^ 2 = 0

Adapted from #4518 @Kevin Lacker

[Heather Macbeth]

(Maybe this is overkill, but would a Grobner basis tactic do this?)

[Mario Carneiro]

I think this is where a Grobner basis tactic would do well. Here is me putting in the coefficients myself:

import data.real.basic

example (a : ℝ) :
  a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1
  ↔ a * (a ^ 2 - 1 / 2) * (4 * a ^ 3 - 3 * a) = 0 :=
begin
  rw ← sub_eq_zero,
  conv {to_rhs, rw ← mul_right_inj' (by norm_num : (4 : ℝ) ≠ 0) },
  congr'; ring
end

[Heather Macbeth]

Note that when I studied the full problem in #4518, I found myself wanting to take the radical of an ideal; will the Grobner basis tactic do this too?

[Kevin Buzzard]

I'm not so sure. Groebner bases answer the question "is this specific multivariable polynomial in this ideal generated by these specific multivariable polynomials" and hence can prove goals of the form " f(x,y,z)=0 and g(x,y,z)=0 implies h(x,y,z)=0" when h is in the ideal generated by f and g. In a general ring, if a^2=0 it doesn't imply that a=0. However it feels like a very similar kind of question -- if you want to prove that h^3 is in the ideal generated by f and g then this is groebner too, but you'll have to come up with the number 3 yourself perhaps.