-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem peval_polyOfInterest (n : ℕ) (x y : 𝕎 k) :
    peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
    (x * y).coeff (n + 1) + p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
      y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
simp only [polyOfInterest, peval, map_natCast, Matrix.head_cons, map_pow,
  Function.uncurry_apply_pair, aeval_X, Matrix.cons_val_one, map_mul, Matrix.cons_val_zero,
  map_sub]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        x.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
            ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) -
      y.coeff (n + 1) *
        (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        x.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
            ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) -
      y.coeff (n + 1) *
        (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
rw [sub_sub, add_comm (_ * _), ← sub_sub]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        y.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
            ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      x.coeff (n + 1) *
        (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        y.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
            ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      x.coeff (n + 1) *
        (aeval (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i]))
          ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
simp [wittPolynomial_eq_sum_C_mul_X_pow, aeval, eval₂_rename, mul_coeff, peval, map_natCast,
  map_add, map_pow, map_mul]

Result:
no goals