Simple lemma with irreducible polynomial factors

Stream: maths

[Ingmar Velien]

Proof assistants, and Lean, are completely new to me.

1. How can I derive the following simple lemma in Lean?
2. How can I let Lean check if the lemma is efficiently written?

This lemma is my first trial to read and write things with Lean. I already know Lean documentation and introductions, but I couldn't find the answers to my questions and the starting point.

Lemma:
Let $P(X,Y)\in\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}}$ does not contain factors $p_X(X)\in\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}}$ and does not contain factors $p_Y(Y)\in\overline{\mathbb{Q}}[Y]\setminus\overline{\mathbb{Q}}$.
There are an $n\in\mathbb{N}_+$ and $\overline{\mathbb{Q}}$-irredcucible $P_1(X,Y),...,P_n(X,Y)\in\overline{\mathbb{Q}}[X,Y]\setminus\overline{\mathbb{Q}}[X]\setminus\overline{\mathbb{Q}}[Y]$ so that the equation $P(x,y)=0$ is splitting into the equations $P_1(x,y)=0,...,P_n(x,y)=0$.

I already got the answer "mv_polynomial (fin 2) algebraic_closure ℚ", but I don't know how to start.

[Yaël Dillies]

Use $$ $$ :smile: