Proof of unsolvability of equations by elementary functions

Stream: new members

[Justus Willbad]

From GitHub CoPilot, I got the following code for my theorem.
Lean gives the error notes below. Could you please help to correct the code?
Maybe there is still Lean 3 code in it?

import Mathlib

open Polynomial
open Classical

def algebraicallyIndependent (f1 f2 : ℂ → ℂ) : Prop :=
  ∀ (P : Polynomial (ℂ × ℂ)), P.eval (f1, f2) = 0 → P = 0


def is_elementary (f : ℂ → ℂ) : Prop :=
∃ g : (ℂ → ℂ), g = f -- simplified definition

theorem no_elementary_solution
  (P : Polynomial (ℂ × ℂ)) (f1 f2 : ℂ → ℂ) (h_independence : algebraically_independent f1 f2) :
  ¬ ∃ (g : ℂ → ℂ), is_elementary g ∧ (∃ (f1_inv f2_inv : ℂ → ℂ),
    is_elementary f1_inv ∧ is_elementary f2_inv ∧
    ∀ x, P.eval (f1 x, f2 x) = 0 → x = g (f1_inv (f2 x))) := sorry

Rearranging.lean:8:30
application type mismatch
eval (f1, f2) P
argument
P
has type
(ℂ × ℂ)[X] : Type
but is expected to have type
((ℂ → ℂ) × (ℂ → ℂ))[X] : Type

Rearranging.lean:15:61
function expected at
algebraically_independent
term has type
?m.1608

[Ruben Van de Velde]

What error?

[Justus Willbad]

I added this above now.

[Ruben Van de Velde]

That seems pretty obvious - you have a polynomial over \C \times \C and try to evaluate it on two functions

[Ruben Van de Velde]

I suggest you step away from copilot

[Justus Willbad]

It want to have the polynomial $P(X,Y)\in \mathbb{K}[X,Y]$ and then $P(f1(x),f2(x))$.

[Aaron Liu]

You can try using docs#Prod.map, so eval (Prod.map f1 f2) P (not tested).
EDIT: this doesn't work

[Justus Willbad]

I changed to eval (Prod.map f1 f2). What should I write in the last row for P.eval (f1 x, f2 x)?

[Aaron Liu]

Justus Willbad said:

It want to have the polynomial $P(X,Y)\in \mathbb{K}[X,Y]$ and then $P(f1(x),f2(x))$.

In Lean you have $P(X) \in (\mathbb{C} \times \mathbb{C})[X]$ where $\mathbb{C} \times \mathbb{C}$ is the set of pairs of complex numbers, with addition and multiplication given pointwise.

[Aaron Liu]

If you want a multivariate polynomial I suggest you go look at docs#MvPolynomial.

[Ruben Van de Velde]

In any case you'd write (f1 x, f2 x), not (f1, f2)