-- Mathlib/RingTheory/WittVector/MulP.lean
theorem mulN_coeff (n : ℕ) (x : 𝕎 R) (k : ℕ) :
    (x * n).coeff k = aeval x.coeff (wittMulN p n k)

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ peval (wittAdd p k) ![(x * ↑n).coeff, x.coeff] =
    (aeval fun i => (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] = fun i => (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑(n + 1)).coeff k = (aeval x.coeff) (wittMulN p (n + 1) k)

Tactic:
rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ peval (wittAdd p k) ![(x * ↑n).coeff, x.coeff] =
    (aeval fun i => (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)

Proof state:
case h.mk
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
b : Fin 2
i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] (b, i) = (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] (b, i))

Tactic:
fin_cases b

Result:
case h.mk.«0»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i => i) ⟨0, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i => i) ⟨0, ⋯⟩, i))

case h.mk.«1»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i => i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i => i) ⟨1, ⋯⟩, i))

Proof state:
case h.mk.«0»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i => i) ⟨0, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i => i) ⟨0, ⋯⟩, i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_zero, ih]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)

Tactic:
induction' n with n ih generalizing k

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑0).coeff k = (aeval x.coeff) (wittMulN p 0 k)

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑(n + 1)).coeff k = (aeval x.coeff) (wittMulN p (n + 1) k)

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑0).coeff k = (aeval x.coeff) (wittMulN p 0 k)

Tactic:
simp only [Nat.cast_zero, mul_zero, zero_coeff, wittMulN, Pi.zero_apply, map_zero]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] = fun i => (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)

Tactic:
ext1 ⟨b, i⟩

Result:
case h.mk
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
b : Fin 2
i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] (b, i) = (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] (b, i))

Proof state:
case h.mk.«1»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i => i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i => i) ⟨1, ⋯⟩, i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_one, Matrix.head_cons, aeval_X]

Result:
no goals