theory Scratch
  imports Main
begin 

lemma ideal_membership_2:
  fixes x0 x1 y0 y1 t :: "'b::idom"
  assumes "x0 ≠ 0" "y0 ≠ 0" "x1 ≠ 0" "y1 ≠ 0"
  shows "∃ q1 q2 q3 q4.
          y0^2 - x1^2 =
              q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) +
              q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) +
              q3*(x0 * y0 - x1 * y1) +
              q4*(x1 * y0 + x0 * y1)"
  using assms apply algebra
(*
Exception trace - exception Option raised (line 82 of "General/basics.ML")
  Groebner.ring_and_ideal_conv(10)solve_idealism (line 872 of "/home/makarius/isabelle/repos/src/HOL/Tools/groebner.ML")
  Groebner.ideal_tac(3)(2)poly_exists_tac (line 959 of "/home/makarius/isabelle/repos/src/HOL/Tools/groebner.ML") 
exception Option raised (line 82 of "General/basics.ML")
*)

end