Finding closed forms for various addition laws on elliptic curves, FullSimplify fails even with assumptions?

Question

I would like to get Mathematica to do some tedious algebra for me, but I have been unsuccessful so far, and I don't know whether I am not using it correctly or whether it is simply not sophisticated enough, so I would like to know if there is a way to make Mathematica find these closed forms "on its own".

I will illustrate my problem with a very simple example. Let's say I have the equation of some curve, say $y^2-x^3 = c$ (sometimes known as Bachet's equation).

I would like to do the following: pretend $(x,y)$ is a solution (with $y \neq 0$ to avoid some problems), then I would like to compute the coordinates of the intersection (different from $(x,y)$) of Bachet's curve with its tangent at $(x,y)$. (There is only one)

Doing this involves solving a system of non-linear equations. If the coordinates I am looking for are $(X,Y)$, then we have

$Y^2-X^3 = c$ (the point lies on Bachet's curve), and we also have

$2y(Y-y)-3x^2(X-x) =0$ (the point lies on the tangent), with the assumption that

$y^2-x^3=c$ ($(x,y)$ is a solution)

The problem : apparently, Mathematica succeeds in solving this system of equations for $(X,Y)$ using Solve. However, FullSimplify does not seem to work as intended. I already know the formula and the output is supposed to be $(X,Y) = (\frac{x^4-8cx}{4y^2},\frac{-x^6-20cx^3+8c^2}{8y^3})$, but I am not getting this no matter how I use assumptions. My attempt it the following:

$\text{FullSimplify}\left[\text{Solve}\left[\left\{2 y (Y-y)-3 x^2 (X-x)=0,-c-X^3+Y^2=0\right\},\{X,Y\}\right],\left\{y^2-x^3=c,x\in \mathbb{Q},y\in \mathbb{Q},c\in \mathbb{Q},X\in \mathbb{Q},Y\in \mathbb{Q},y\neq 0\right\}\right]$

Plain text:

Clear[x,y,X,Y,c]
FullSimplify[Solve[{2*y*(Y-y)-3*x^2*(X-x)==0,Y^2-X^3-c==0},{X,Y}],
 {y^2-x^3==c,{x, y, c, X, Y} ∈ Rationals,y!=0}]

It yields the correct formula but fails to simplify to the expected simple formula. The fact that it can solve a non-linear system of equation but fails to simplify makes me think there is some hope left, but perhaps this is just too advanced for Mathematica and I will have to do it myself (I know that the formulas are known and catalogued in the literature, but I wanted to experiment with other things)

Is there a way to simplify further or did I just reach Mathematica's limits?

If it helps, Mathematica returns the following instead:

$\left\{X\to \frac{-9 c^2 x^2+3 x y^2 \sqrt[3]{\left(y^2-c\right) \left(3 c+y^2\right)^3}-3 c x \left(\sqrt[3]{\left(y^2-c\right) \left(3 c+y^2\right)^3}+2 x y^2\right)-\left(\left(y^2-c\right) \left(3 c+y^2\right)^3\right)^{2/3}-x^2 y^4}{4 y^2 \sqrt[3]{\left(y^2-c\right) \left(3 c+y^2\right)^3}},Y\to \frac{9 c^2-3 x^2 \sqrt[3]{\left(y^2-c\right) \left(3 c+y^2\right)^3}-\frac{3 x \left(\left(y^2-c\right) \left(3 c+y^2\right)^3\right)^{2/3}}{3 c+y^2}-6 c y^2+5 y^4}{8 y^3}\right\}$

(with two other expressions for $(X,Y)$ which should correspond to $(x,y)$ and are not interesting. Mathematica also fails to simplify those and gives enormous formulas for what is supposed to be simply $(x,y)$, since a tangent is the geometric equivalent of a multiple root (here, double root))

Answer 1

We can give FullSimplify some help by allowing for PowerExpand rules and manually performing a substitution:

laxSimplify[args__] := 
  FullSimplify[args, TransformationFunctions -> {Automatic, PowerExpand}]

sol = Solve[{2*y*(Y - y) - 3*x^2*(X - x) == 0, Y^2 - X^3 - c == 0}, {X, Y}][[1]];

Assuming[
  {y^2 - x^3 == c, {x, y, c, X, Y} ∈ Rationals, y != 0},
  laxSimplify[laxSimplify[sol] /. y^2 -> c + x^3]
]

$\left\{X\to \frac{1}{4} \left(x-\frac{9 c x}{y^2}\right),Y\to \frac{1}{8} \left(\frac{27 c^2}{y^3}-\frac{18 c}{y}-y\right)\right\}$