Polymonial proof

Stream: general

[Jiatong Gao]

have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
    sorry

i want to ask how to prove this thing, I have no idea.
below is I defined

  let P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
  let x : Fin 3 → ℤ := ![1, 2, 4]

[Jiatong Gao]

I tried to cases it

  have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
    intro i
    fin_cases i
    · -- i = 0, x 0 = 1
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num
    · -- i = 1, x 1 = 2
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num
    · -- i = 2, x 2 = 4
      simp [x, P, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_sub,
            Polynomial.eval_X, Polynomial.eval_C]
      norm_num

But failed, it says that

unsolved goals
case «0»
P : ℤ[X] := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
x : Fin 3 → ℤ := ![1, 2, 4]
y : Fin 2 → ℤ := ![0, 3]
h_x : ∀ (i j : Fin 3), i ≠ j → x i ≠ x j
h_y : ∀ (i j : Fin 2), i ≠ j → y i ≠ y j
⊢ False

[Ilmārs Cīrulis]

That's because the value of the polynomial in each case is 2013, not 54, probably?

import Mathlib
open Polynomial

noncomputable def P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013

def x : Fin 3 → ℤ := ![1, 2, 4]

theorem h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 2013 := by
  unfold P x
  intro i
  fin_cases i <;> simp

[Jiatong Gao]

Thanks a lot, there is full process now,I am the beginner and confused about how to figure there two polynomial out

import Mathlib
open Polynomial

/- Let $k$ and $n$ be positive integers and let $x_{1}, x_{2}, \ldots, x_{k}, y_{1}, y_{2}, \ldots, y_{n}$ be distinct integers. A polynomial $P$ with integer coefficients satisfies

$$
P\left(x_{1}\right)=P\left(x_{2}\right)=\ldots=P\left(x_{k}\right)=54
$$

and

$$
P\left(y_{1}\right)=P\left(y_{2}\right)=\ldots=P\left(y_{n}\right)=2013 .
$$

Determine the maximal value of $k n$. -/
theorem algebra_604776 :
  ∃ (k n : ℕ),
    0 < k ∧ 0 < n ∧
    ∃ (x : Fin k → ℤ) (y : Fin n → ℤ),
      (∀ i j : Fin k, i ≠ j → x i ≠ x j) ∧
      (∀ i j : Fin n, i ≠ j → y i ≠ y j) ∧
      ∃ (P : Polynomial ℤ),
        (∀ i, P.eval (x i) = 54) ∧
        (∀ i, P.eval (y i) = 2013) ∧
        k * n = 6 := by
  let P : Polynomial ℤ := 653 * ((X - C 1) * (X - C 2) * (X - C 4)) + C 2013
  let x : Fin 3 → ℤ := ![1, 2, 4]
  let y : Fin 2 → ℤ := ![0, 3]
  have h_x : ∀ i j : Fin 3, i ≠ j → x i ≠ x j := by
    intros i j hij
    fin_cases i <;> fin_cases j
    · contradiction
    · dsimp [x]; decide
    · dsimp [x]; decide
    · dsimp [x]; decide
    · contradiction
    · dsimp [x]; decide
    · dsimp [x]; decide
    · dsimp [x]; decide
    · contradiction


  have h_y : ∀ i j : Fin 2, i ≠ j → y i ≠ y j := by
    intros i j hij
    fin_cases i <;> fin_cases j
    · contradiction
    · dsimp [y]; decide
    · dsimp [y]; decide
    · contradiction

  have h_Px : ∀ i : Fin 3, Polynomial.eval (x i) P = 54 := by
    sorry

  have h_Py : ∀ i, Polynomial.eval (y i) P = 2013 := by
    sorry


  exact ⟨3, 2,
  ⟨by decide, by decide,
    ⟨x, y,
      ⟨h_x, h_y,
        ⟨P, ⟨h_Px, h_Py, by norm_num⟩⟩⟩⟩⟩⟩