(need help) an example property of Polynomial.coeff

Stream: mathlib4

[Zhu]

I'm attempting to prove an 'apparent' property, but I've got stuck. Here's the code I have so far.

import Mathlib
open Polynomial

example
    (p : ℝ[X])
    (h : ∀ x, p.eval (3 * x) + p.eval (5 * x) - 3 * p.eval (2 * x) = 0) :
    ∀ i : ℕ, p.coeff i * (3 ^ i + 5 ^ i - 3 * 2 ^ i) = 0 := by

  simp only [Polynomial.eval_eq_sum_range, ← Finset.sum_add_distrib, Finset.mul_sum, ← Finset.sum_sub_distrib, ← mul_add] at h
  simp_rw [mul_left_comm (3 : ℝ), ← mul_sub, mul_pow, ← mul_assoc, ← add_mul, ← sub_mul, ← mul_assoc] at h

  -- set n := p.natDegree
  -- set g : ℕ → ℝ := fun i => p.coeff i * (3 ^ i + 5 ^ i - 3 * 2 ^ i)
  -- have : ∀ x : ℝ, ∑ i ∈ Finset.range (n + 1), g i * x ^ i = 0 := by
  --   convert h
  sorry

I think the rest might be provable through induction on p.natDegree, but is there any simpler way to use Polynomial API to prove this?

By the way, Is there any tutorial available on using the Polynomial API in Lean4?

[Yury G. Kudryashov]

You will need docs#Polynomial.funext

[Yury G. Kudryashov]

You should prove that the polynomial p.comp (.C 3 * .X) + p.comp (.C 5 * .X) - .C 3 * p.comp (.C 2 * .X) has coefficients 3 ^ i + 5 ^ i - 3 * 2 ^ i, then apply Polynomial.funext.

[Yury G. Kudryashov]

I don't remember if we have a lemma about the coefficients of p.comp (.C _ * .X)

[Yury G. Kudryashov]

We do, see Polynomial.comp_C_mul_X_coeff

[Zhu]

Thanks! I managed to complete the proof based on your hints. Here's the code:

import Mathlib
open Polynomial

example
    (p : ℝ[X])
    (h : ∀ x, p.eval (3 * x) + p.eval (5 * x) - 3 * p.eval (2 * x) = 0) :
    ∀ i : ℕ, p.coeff i * (3 ^ i + 5 ^ i - 3 * 2 ^ i) = 0 := by

  set q : ℝ[X] := p.comp (.C 3 * .X) + p.comp (.C 5 * .X) - .C 3 * p.comp (.C 2 * .X)

  have heq : q = 0 := by
    apply Polynomial.funext
    simp [q]
    intro x
    convert h x

  have hcoeff : ∀ i, q.coeff i = p.coeff i * (3 ^ i + 5 ^ i - 3 * 2 ^ i) := by
    intro i
    simp [q]
    ring_nf

  intro i
  rw [← hcoeff i, show (0:ℝ) = Polynomial.coeff 0 i by rfl, heq]