How to solve problems like the method of comparing coefficie

Stream: mathlib4

[言绎心]

How to solve problems like the method of comparing coefficients?
Problem 1: Determine the possible values of each unknown variable through unique factorization.
Problem 2: Vieta’s formula for higher-degree polynomials (degree > 2).
Problem 3: Compare different coefficients to determine the values of x .

import Mathlib

example {a b c : ℕ} (h₁ : (a - 1) * (b - 1) * (c - 1) = 2 * 3 * 5) (h₂ : a + b + c = 13) :
  a * b * c = 72 := by sorry

/-
example {x₁ x₂ x₃ : ℂ} {f : ℂ → ℂ}
  (hx₁ : f x₁ = 0) (hx₂ : f x₂ = 0) (hx₃ : f x₃ = 0)
  (hf : ∀x, f x = x * x * x - 2 * x * x - 2 * x + 2) :
  x₁ * x₂ * x₃ = 2 := by sorry
-/

-- Another version
example {a b c : ℂ} (ha : a.im = 0) (h1 : a + b + c = 3) (h2 : a * b + b * c + c * a = 3)
    (h3 : a * b * c = 3) : a = 1 + 2 ^ ((1 : ℂ) / 3) := by sorry
-- By Vieta's formula, a, b, c is the root of x^3 - 3x^2 - 3x - 3 = 0
-- so, (x-1)^3 = 2


example {x : ℂ} (h: ∀z, z^3 + x^2 * z^2 + x * z = x^2 * z^3 + x * z^2 + z) : x = 1 := by
  sorry

These problems look quite intuitive, but when I try to formalize them using Lean4, they become tricky.  
In comparison, for solving a univariate polynomial equation, I can easily compute most of the roots, then rewrite it in a factorized form like $(x-a)(x-b)(x-c)$, and directly obtain $x = a \vee x = b \vee x = c$.

[言绎心]

It seems that example 2 is not entirely rigorous, but I don't know how to express it rigorously in Lean4.
Lean4 warns me that { x : ℂ | f x = 0 } is not Fintype ℂ in ∏x∈{ x : ℂ | f x = 0 }, x = 2

[Kevin Buzzard]

The first one will certainly be tricky to formalise -- what about a=31,b=c=2?

[Kevin Buzzard]

Similarly the second problem is also not true as it stands, as there's nothing stopping x1=x2=x3

[言绎心]

Kevin Buzzard said:

The first one will certainly be tricky to formalise -- what about a=31,b=c=2?

As for the first question, this is actually a key step in a complete problem. Specifically, the full condition of the original question should be:

import Mathlib

example {a b c : ℕ} (h₁ : (a - 1) * (b - 1) * (c - 1) = 2 * 3 * 5) (h₂ : a + b + c = 13) :
  a * b * c = 72 := by sorry

You've reminded me that removing one condition makes the answer non-unique. For this type of problem, aside from exhaustive search, there doesn't seem to be a better approach. As long as humans can find a solution only, the problem can be considered solved. After formalizing it, Lean4 will inevitably assert that no other solutions exist.

[言绎心]

Kevin Buzzard said:

The first one will certainly be tricky to formalise -- what about a=31,b=c=2?

As for the second question, I really can't think of an appropriate expression. After all, Gauss proved that a polynomial of degree n has n roots in the complex field, but this doesn't prevent the roots from being equal. In fact, even using 'prod' wouldn't be appropriate, because the root set is a set, and the elements of a set are unique. For example, the root set of $(x-2)^2$ is $\{2\}$, but according to Vieta's formulas, $x_1 \cdot x_2 = 4$.

[言绎心]

I believe the second type of problem is difficult to prove, I can't think of a better way besides doing this

The prove of example 2:

example {a b c : ℂ} (ha : a.im = 0) (h1 : a + b + c = 3) (h2 : a * b + b * c + c * a = 3)
    (h3 : a * b * c = 3) : a = 1 + 2 ^ ((1 : ℂ) / 3) := by
  have eq : ∀x, (x - a) * (x - b) * (x - c) =
          x^3 - (a + b + c) * x^2 + (a * b + b * c + c * a) *x - a * b * c := by
      intro x
      ring_nf

  rw [h1, h2, h3] at eq
  have : (a - 1)^3 = (a^3 - 3 * a^2 + 3 * a - 3) + 2 := by ring_nf
  have p : (a - 1)^3 = 2 := by
    rw [this, (eq a).symm, sub_self]
    simp

  -- Although a = 1 + 2^(1/3) is obvious, but, it is difficult to prove it.
  rw [Complex.cpow_def]
  have ha' : a.re = a := by
    exact Complex.ext rfl (id (Eq.symm ha))
  -- split `if` of cpow
  split
  . -- if 2 = 0, which is impossible
    rename_i h
    absurd h
    simp
  . -- 2 ≠ 0
    -- replace `2` to `a - 1`, and expand log
    rw [p.symm, Complex.log]
    -- prove ((a - 1) ^ 3).arg is 0
    have : ((a - 1) ^ 3).arg = 0 := by
      rw [p]
      simp
    rw [this]
    field_simp
    rw [Complex.abs_eq_sqrt_sq_add_sq]
    have : (a - 1).im = 0 := by
      rw [Complex.sub_im, Complex.one_im, ha]
      simp
    rw [this]
    simp
    norm_cast

    -- this part is condition of `sqrt_sq` and `exp_log`
    have : (a.re - 1) ^ 3 = (2 : ℂ) := by
      rw [p.symm]
      rw [ha']
    norm_cast at this
    have : (a.re - 1) ^ 3 > 0 := by linarith
    have : 0 < a.re - 1 := by
      have h : Odd 3 := by norm_cast
      apply (Odd.pow_pos_iff h).mp
      linarith

    -- now, we need to prove a = ↑(1 + Real.exp (Real.log √((a.re - 1) ^ 2)))
    rw [Real.sqrt_sq this.le, Real.exp_log this]
    simp
    exact ha'.symm