Filling in the proof of ‘IsUnit f’

Stream: new members

[Nick_adfor]

I was trying to formalize "No polynomial ring with more than one indeterminant is a PID.

Now the construction has been already done. If I give have: IsUnit f := by sorry, then there's no error. But now I have question about filling in IsUnit f. First, I don't know how to fill these sorrys. Second, I don't know how to continue after exact (before to be continued). So I ask for your kindness help, thanks!

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]



theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by

  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j


  let I := span ({x, y} : Set (MvPolynomial σ R))

  intro hPID

  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal


  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  rw [hf] at x_mem y_mem

  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem

  have unit_f: IsUnit f := by
    have h_mul_zero_x : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_x
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_x
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 a = 0 := by
        rw [← h_mul_zero_x, ← coeff_zero_X i]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    have h_mul_zero_y : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_y
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_y
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 b = 0 := by
        rw [← h_mul_zero_y, ← coeff_zero_X j]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    by_cases ha0 : coeff (0 : σ →₀ ℕ) a ≠ 0
    · have f0 := coeff_f_zero_of_a ha0
      have f_dvd_Xi : f ∣ x := by
        use a
      obtain ⟨g, rfl⟩ : ∃ g, f = x * g := by
        have a_decomp: a = C (a.coeff 0) + (a - C (a.coeff 0)) := by simp
        have key_eq : f * C (a.coeff 0) = x - f * (a - C (a.coeff 0)) := by
          rw [ha]
          ring
        refine ⟨a * (C (a.coeff 0)⁻¹), ?_⟩
        have const_zero : coeff 0 f = 0 := coeff_f_zero_of_a ha0
        have zero_term : f * (a - C (a.coeff 0)) = 0 := by sorry
        rw [zero_term, sub_zero] at key_eq
        have : f = x * (a * C (a.coeff 0)⁻¹) := by
          sorry
        exact this
      have : x * g ∣ y := by rw [hb]; exact dvd_mul_right (x * g) b
      have dvd_x_y: x ∣ y := by
        apply dvd_trans (dvd_mul_right x g) this
      have eq_ij : i = j := by
        sorry
      contradiction

    by_cases hb0 : coeff (0 : σ →₀ ℕ) b ≠ 0
    · have f0' := coeff_f_zero_of_b hb0
      have f_dvd_Yi : f ∣ y := by
        use b
      obtain ⟨g', rfl⟩ : ∃ g', f = y * g' := by
        have b_decomp: b = C (b.coeff 0) + (b - C (b.coeff 0)) := by simp
        have key_eq' : f * C (b.coeff 0) = y - f * (b - C (b.coeff 0)) := by
          rw [hb]
          ring
        refine ⟨b * (C (b.coeff 0)⁻¹), ?_⟩
        have const_zero' : coeff 0 f = 0 := coeff_f_zero_of_b hb0
        have zero_term' : f * (b - C (b.coeff 0)) = 0 := by sorry
        rw [zero_term', sub_zero] at key_eq'
        have : f = y * (b * C (b.coeff 0)⁻¹) := by
          sorry
        exact this
      have : y * g' ∣ x := by rw [ha]; exact dvd_mul_right (y * g') a
      have dvd_y_x: y ∣ x := by
        apply dvd_trans (dvd_mul_right y g') this
      have eq_ij : i = j := by
        sorry
      contradiction

    have coeff_a0 : coeff 0 a = 0 := by
      by_contra ha0'
      exact ha0 ha0'
    have coeff_b0 : coeff 0 b = 0 := by
      by_contra hb0'
      exact hb0 hb0'
    have rhs_zero : coeff 0 (f * a + f * b) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp [coeff_a0, coeff_b0]
    have one_eq : 1 = f * a + f * b := by
      sorry
    have coeff_eq : coeff 0 1 = coeff 0 (f * a + f * b) := congr_arg (coeff 0) one_eq
    rw [rhs_zero] at coeff_eq
    have coeff_one_zero: coeff (0 : σ →₀ ℕ) 1 = 1 := coeff_one (0 : σ →₀ ℕ)
    exact
    --to be continued

  have proper : I ≠ ⊤ := by
    intro hI
    have one_mem : (1 : MvPolynomial σ R) ∈ I := by rw [hI]; trivial

    obtain ⟨a, b, eq1⟩ := mem_span_pair.mp one_mem

    have const_eq : coeff (0 : σ →₀ ℕ) 1 = coeff (0 : σ →₀ ℕ) (a * x + b * y) := by
      rw [eq1]

    have coeff_x_zero : coeff (0 : σ →₀ ℕ) x = 0 := by
      rw [@coeff_zero_X]

    have coeff_y_zero : coeff (0 : σ →₀ ℕ) y = 0 := by
      rw [@coeff_zero_X]

    have rhs_const : coeff (0 : σ →₀ ℕ) (a * x + b * y) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp
      rw [coeff_x_zero, coeff_y_zero]
      simp

    rw [coeff_one, rhs_const] at const_eq
    exact one_ne_zero const_eq

  have I_eq_top : I = ⊤ := by
    rw [hf]
    change Ideal.span {f} = ⊤
    rw [Ideal.span_singleton_eq_top]
    exact unit_f


  contradiction

[Ruben Van de Velde]

For "to be continued":

    have coeff_one_zero: coeff (0 : σ →₀ ℕ) (1 : MvPolynomial σ R) = 1 := coeff_one (0 : σ →₀ ℕ)
    exfalso
    apply one_ne_zero (α := R)
    rw [← coeff_eq, ← coeff_one_zero]

[Nick_adfor]

exfalso and exact will both generate a False, but exact seem to be used only in the end of the proof. Maybe I'm not so familiar with it. Very thanks!

Now the most difficult part comes to line 83

have eq_ij : i = j := by
        sorry

I used to think that it can be automatically proved by lean, but it cannot : (

[Kenny Lau]

@Nick_adfor docs#MvPolynomial.X_dvd_X

[Kenny Lau]

you can find this by doing @loogle MvPolynomial.X, "dvd"

[loogle]

:search: MvPolynomial.X_dvd_X, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, and 1 more

[Nick_adfor]

Thanks for that! And also from line 67-78, I want to obtain a g by hand (I may also think that it cannot be proved automatically by lean.) But as one can see, to construct a C (a.coeff 0)⁻¹ might cause some type conversion issues. So I use two sorry here.

      obtain ⟨g, rfl⟩ : ∃ g, f = x * g := by
        have a_decomp: a = C (a.coeff 0) + (a - C (a.coeff 0)) := by simp
        have key_eq : f * C (a.coeff 0) = x - f * (a - C (a.coeff 0)) := by
          rw [ha]
          ring
        refine ⟨a * (C (a.coeff 0)⁻¹), ?_⟩
        have const_zero : coeff 0 f = 0 := coeff_f_zero_of_a ha0
        have zero_term : f * (a - C (a.coeff 0)) = 0 := by sorry
        rw [zero_term, sub_zero] at key_eq
        have : f = x * (a * C (a.coeff 0)⁻¹) := by
          sorry
        exact this

[Kenny Lau]

@Nick_adfor there are no type issues because your coefficients live in the field R

[Kenny Lau]

also sorry but i don't understand what your question is.

[Kenny Lau]

is there a math proof (segment) that you're trying to convert?

[Nick_adfor]

Proving the generator f must be a unit:

Substep 1 (Constant term analysis):
From the equations:
X_i = f·a
X_j = f·b

Looking at constant terms (coeff 0):

1. coeff 0 f · coeff 0 a = 0 (since coeff 0 X_i = 0)
2. coeff 0 f · coeff 0 b = 0 (since coeff 0 X_j = 0)

Substep 2 (Case breakdown):

• Case A: If coeff 0 a ≠ 0
  From equation 1: coeff 0 f = 0 ⇒ f has no constant term
  Since f divides X_i ⇒ f must be associate to X_i (f = u·X_i, u is unit)
  But f divides X_j ⇒ X_i divides X_j ⇒ i = j, contradicting i ≠ j

• Case B: If coeff 0 b ≠ 0
  Same contradiction as Case A by symmetry

• Case C: coeff 0 a = coeff 0 b = 0
  From X_i = f·a, since a has no constant term, f must provide it ⇒ f must be invertible
  (Because 1 ∈ (f) ⇒ exists c where f·c = 1 ⇒ f is unit)

[Kenny Lau]

@Nick_adfor ok, and which step are you stuck on? it would be more helpful (to both of us) if you could be more specific in your questions

[Nick_adfor]

Now I want to construct g = a * (C (a.coeff 0))⁻¹. It is refine ⟨a * (C (a.coeff 0)⁻¹), ?_⟩ in the code.

[Kenny Lau]

ok, but where did you get stuck? for example, I don't see any mention of "g" in the pen-and-paper proof that you just provided. I hope you understand my frustration here with trying to help you.

[Nick_adfor]

Sorry for that. I'm now stuck in filling in the two sorry.

Given Conditions

1. Let x = Xᵢ (the polynomial for the i-th variable)
2. Given the relation x = f·a
3. The constant term of polynomial a is non-zero (a₀ ≠ 0 where a₀ = coeff₀(a))
4. The constant term of polynomial f is zero (coeff₀(f) = 0)

Goal
Construct a polynomial g such that f = x·g

Proof Steps

1. Polynomial Decomposition
   Decompose a into constant and non-constant parts:
   a = a₀ + (a - a₀)
   Where:
   a₀ = coeff₀(a) is the constant term
   (a - a₀) is the polynomial with the constant term removed

2. Relation Expansion
   Substitute into x = f·a:
   x = f·a₀ + f·(a - a₀)
   Rearranged as:
   f·a₀ = x - f·(a - a₀)

3. Key Product Vanishing
   Prove f·(a - a₀) = 0:
   Since coeff₀(f) = 0 and coeff₀(a - a₀) = 0
   For any monomial Xᵈ, the coefficient sum:
   ∑_{k+l=d} coeffₖ(f)·coeffₗ(a - a₀) = 0
   When k=0, coeff₀(f)=0 makes term vanish
   When k≠0, non-Xᵢ terms have zero coefficients

4. Simplified Relation
   Substituting f·(a - a₀) = 0 gives:
   f·a₀ = x

5. Construction of g
   Since a₀ ≠ 0, its inverse a₀⁻¹ exists (assuming R is field or a₀ invertible)
   Define:
   g = a₀⁻¹
   Then:
   f = x·a₀⁻¹ = x·g
   Verification:
   x·g = x·a₀⁻¹ = (f·a₀)·a₀⁻¹ = f·(a₀·a₀⁻¹) = f·1 = f

Conclusion
We constructed g = a₀⁻¹ satisfying f = x·g.

[Kenny Lau]

@Nick_adfor ok, i tried to read your pen-and-paper proof, and i got stuck on step 3.

When k≠0, non-Xᵢ terms have zero coefficients

what is the proof of this? non-Xi terms of what? what about the Xi terms?

[Nick_adfor]

It is that maybe some of the proof I've given is wrong so I cannot fill the sorry. So maybe step 3 is where the wrong part begins.

[Kenny Lau]

i thought you're formalising a proof you already have; or is this not the case?

[Kenny Lau]

right, that step is actually wrong for f=1 and a=Xi, since then a0=0 and f.(a-a0) = Xi

[Nick_adfor]

Oh...So is it that I need to change the way to try sorry?

[Nick_adfor]

It's terrible that I'm at UTC+8 and it's now 1 a.m. so it's too hard for me to think. I'm quite sorry for your frustration.

[Kenny Lau]

you can always come back tomorrow

[Nick_adfor]

My construction of g might be a little more confusing. Should I try another way?

[Nick_adfor]

Ruben Van de Velde said:

For "to be continued":

    have coeff_one_zero: coeff (0 : σ →₀ ℕ) (1 : MvPolynomial σ R) = 1 := coeff_one (0 : σ →₀ ℕ)
    exfalso
    apply one_ne_zero (α := R)
    rw [← coeff_eq, ← coeff_one_zero]

This part really helps to accomplish the proof structure, thanks : )

[Nick_adfor]

Maybe have zero_term : f * (a - C (a.coeff 0)) = 0 := by sorry should be replaced. For example, I can let f to be c * x + d * y, and rw x = f * a, y = f * b to try to find a contradiction. But it need to prove from x | f * y to x | f. I have no idea here.

[Kenny Lau]

Nick_adfor said:

My construction of g might be a little more confusing. Should I try another way?

you should do everything on paper first

[Nick_adfor]

It is that I'm still trying have zero_term

[Nick_adfor]

with no idea

[Kenny Lau]

are you formalising an existing proof, or are you coming up with the proof yourself?

[Nick_adfor]

Kenny Lau said:

are you formalising an existing proof, or are you coming up with the proof yourself?

I'm coming up with the proof myself. The question is to formalize "No polynomial ring with more than one indeterminant is a PID."

[Nick_adfor]

So I have given a structure, but I have never thought of lean cannot automatically construct ∃ g, f = x * g

[Nick_adfor]

And as I check, I do think that have one_eq : 1 = f * a + f * b := by sorry is wrong.

[Nick_adfor]

Now I refresh my code

import Mathlib

open MvPolynomial Ideal

-- We assume R is a field, and σ is a finite type with decidable equality.
variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]

/-- The main theorem: If the number of variables is at least 2, then MvPolynomial σ R is not a PID.-/
theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by

  -- Select two distinct variables i ≠ j from σ, which is possible by assumption on the cardinality.
  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  -- Define the two variables X i and X j in the multivariable polynomial ring.
  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j

  -- Let I be the ideal generated by x and y.
  let I := span ({x, y} : Set (MvPolynomial σ R))

  -- Suppose for contradiction that MvPolynomial σ R is a principal ideal ring.
  intro hPID

  -- Now the ideal I must be principal.
  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal

  -- x and y are in the ideal I.
  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  -- Rewrite using the assumption that I = ⟨f⟩.
  rw [hf] at x_mem y_mem

  -- So x and y are multiples of f.
  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem

  -- Goal: derive that f must be a unit, leading to contradiction.
  have unit_f: IsUnit f := by
    -- Compare constant term of x with that of f * a.
    have h_mul_zero_x : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    -- Since i ≠ j, X i has no constant term.
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_x
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_x

    -- From the constant term of f * a = 0, deduce coeff 0 f = 0 if coeff 0 a ≠ 0.
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 a = 0 := by
        rw [← h_mul_zero_x, ← coeff_zero_X i]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    -- Apply similar logic to y = f * b.
    have h_mul_zero_y : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_y
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_y

    -- Deduce again: coeff 0 f = 0 if coeff 0 b ≠ 0.
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 b = 0 := by
        rw [← h_mul_zero_y, ← coeff_zero_X j]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    -- Split into cases depending on the constant term of a and b.
    by_cases ha0 : coeff (0 : σ →₀ ℕ) a ≠ 0
    · -- Assume constant term of a is nonzero, then coeff 0 f = 0.
      have f0 := coeff_f_zero_of_a ha0
      -- f divides x, so f = x * g for some g.
      have f_dvd_Xi : f ∣ x := by use a
      obtain ⟨g, rfl⟩ : ∃ g, f = x * g := by
        -- Try to construct g = a * (C (a.coeff 0))⁻¹ using cancellation of constant term.
        have a_decomp: a = C (a.coeff 0) + (a - C (a.coeff 0)) := by simp
        have key_eq : f * C (a.coeff 0) = x - f * (a - C (a.coeff 0)) := by
          rw [ha]; ring
        refine ⟨a * (C (a.coeff 0)⁻¹), ?_⟩
        have const_zero : coeff 0 f = 0 := coeff_f_zero_of_a ha0
        have zero_term : f * (a - C (a.coeff 0)) = 0 := by sorry -- To be shown
        rw [zero_term, sub_zero] at key_eq
        have : f = x * (a * C (a.coeff 0)⁻¹) := by sorry -- Need to justify this step
        exact this
      -- From f = x * g and f ∣ y, deduce x ∣ y
      have : x * g ∣ y := by rw [hb]; exact dvd_mul_right (x * g) b
      have dvd_x_y: x ∣ y := by apply dvd_trans (dvd_mul_right x g) this
      -- But then x ∣ y and y ∣ x implies i = j, contradicting distinctness
      have eq_ij : i = j := by
        rw [MvPolynomial.X_dvd_X] at dvd_x_y
        exact dvd_x_y
      contradiction

    by_cases hb0 : coeff (0 : σ →₀ ℕ) b ≠ 0
    · -- Symmetric case to above, assume b has nonzero constant term
      have f0' := coeff_f_zero_of_b hb0
      have f_dvd_Yi : f ∣ y := by use b
      obtain ⟨g', rfl⟩ : ∃ g', f = y * g' := by
        have b_decomp: b = C (b.coeff 0) + (b - C (b.coeff 0)) := by simp
        have key_eq' : f * C (b.coeff 0) = y - f * (b - C (b.coeff 0)) := by
          rw [hb]; ring
        refine ⟨b * (C (b.coeff 0)⁻¹), ?_⟩
        have const_zero' : coeff 0 f = 0 := coeff_f_zero_of_b hb0
        have zero_term' : f * (b - C (b.coeff 0)) = 0 := by sorry -- To be filled
        rw [zero_term', sub_zero] at key_eq'
        have : f = y * (b * C (b.coeff 0)⁻¹) := by sorry
        exact this
      have : y * g' ∣ x := by rw [ha]; exact dvd_mul_right (y * g') a
      have dvd_y_x: y ∣ x := by apply dvd_trans (dvd_mul_right y g') this
      have eq_ij : i = j := by
        rw [MvPolynomial.X_dvd_X] at dvd_y_x
        exact Eq.symm dvd_y_x
      contradiction

    -- Final case: both a and b have zero constant term. If both a and b have zero constant term, then f must be a unit. But I don't know how to handle this case.
    have coeff_a0 : coeff 0 a = 0 := by
      by_contra ha0' ; exact ha0 ha0'
    have coeff_b0 : coeff 0 b = 0 := by
      by_contra hb0' ; exact hb0 hb0'

  -- Now we show I is not the unit ideal.
  have proper : I ≠ ⊤ := by
    intro hI
    have one_mem : (1 : MvPolynomial σ R) ∈ I := by rw [hI]; trivial

    -- If 1 ∈ I, it is a linear combination of x and y.
    obtain ⟨a, b, eq1⟩ := mem_span_pair.mp one_mem

    -- But the constant term of x and y are both zero
    have const_eq : coeff (0 : σ →₀ ℕ) 1 = coeff (0 : σ →₀ ℕ) (a * x + b * y) := by
      rw [eq1]
    have coeff_x_zero : coeff (0 : σ →₀ ℕ) x = 0 := by rw [@coeff_zero_X]
    have coeff_y_zero : coeff (0 : σ →₀ ℕ) y = 0 := by rw [@coeff_zero_X]

    -- Therefore, RHS has constant term 0, contradicting coeff 0 1 = 1
    have rhs_const : coeff (0 : σ →₀ ℕ) (a * x + b * y) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp ; rw [coeff_x_zero, coeff_y_zero]; simp
    rw [coeff_one, rhs_const] at const_eq
    exact one_ne_zero const_eq

  -- If f were a unit, then span {f} = ⊤, contradicting the ideal is proper.
  have I_eq_top : I = ⊤ := by
    rw [hf]
    change Ideal.span {f} = ⊤
    rw [Ideal.span_singleton_eq_top]
    exact unit_f

  contradiction

There's a case I don't know how to prove, and for the other two cases I do not know how to fill the sorry.

[Nick_adfor]

For the final case in unit_f, I don't know how to handle this case.

-- Final case: both a and b have zero constant term. If both a and b have zero constant term, then f must be a unit.
    have coeff_a0 : coeff 0 a = 0 := by
      by_contra ha0' ; exact ha0 ha0'
    have coeff_b0 : coeff 0 b = 0 := by
      by_contra hb0' ; exact hb0 hb0'

I used to construct this way. But it seems that have one_eq : 1 = f * a + f * b := by sorry cannot be proved! So I delete them.

    have coeff_a0 : coeff 0 a = 0 := by
      by_contra ha0'
      exact ha0 ha0'
    have coeff_b0 : coeff 0 b = 0 := by
      by_contra hb0'
      exact hb0 hb0'
    have rhs_zero : coeff 0 (f * a + f * b) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp [coeff_a0, coeff_b0]
    have one_eq : 1 = f * a + f * b := by
      sorry
    have coeff_eq : coeff 0 1 = coeff 0 (f * a + f * b) := congr_arg (coeff 0) one_eq
    rw [rhs_zero] at coeff_eq
    have coeff_one_zero: coeff (0 : σ →₀ ℕ) 1 = 1 := coeff_one (0 : σ →₀ ℕ)
    exfalso
    apply one_ne_zero (α := R)
    rw [← coeff_eq, ← coeff_one_zero]

[Kevin Buzzard]

So just to be clear, lean does not do magic. If it's asking for a proof you can't expect it to magically come up with one by itself, you have to know the proof and then you translate the pen and paper proof into lean.

[Kevin Buzzard]

The systems which find the proof for you are not lean, they are typically some LLM owned by a tech company and which you're not allowed to access right now unless you work for that tech company.

[Nick_adfor]

Nick_adfor said:

So I have given a structure, but I have never thought of lean cannot automatically construct ∃ g, f = x * g

To get a proof in Lean may need more than get a proof by pen-and-paper!

[Kenny Lau]

Nick_adfor said:

To get a proof in Lean may need more than get a proof by pen-and-paper!

That's why you should start with the pen-and-paper proof!

[Nick_adfor]

Correct! I'm still trying on the goal:
Construct a polynomial g such that f = x·g

[Yongle Hu]

Do you have a pen-and-paper proof of constructing g such that f = x * g? I don't think it is mathematically trivial.

[Yongle Hu]

I think a possible proof is that x = f * a implies that either f or a must be invertible since x is a prime element.