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

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ coeff (x * ↑(Nat.succ n)) k = ↑(aeval x.coeff) (wittMulN p (Nat.succ n) k)
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
⊢ coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
induction' n with n ih generalizing k
no goals
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
⊢ coeff (x * ↑Nat.zero) k = ↑(aeval x.coeff) (wittMulN p Nat.zero k)
simp only [Nat.zero_eq, Nat.cast_zero, MulZeroClass.mul_zero, zero_coeff, wittMulN,
  AlgHom.map_zero, Pi.zero_apply]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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)
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ coeff (x * ↑(Nat.succ n)) k = ↑(aeval x.coeff) (wittMulN p (Nat.succ n) k)
rw [wittMulN, Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁,
  add_coeff]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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)
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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)
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
case h.mk
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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))
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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)
ext1 ⟨b, i⟩
case h.mk.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 0, isLt := (_ : 0 < 2) }, i))

case h.mk.tail.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i))
case h.mk
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) 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))
fin_cases b
no goals
case h.mk.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 0, isLt := (_ : 0 < 2) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 0, isLt := (_ : 0 < 2) }, i))
simp [Function.uncurry, Matrix.cons_val_zero, ih]
no goals
case h.mk.tail.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i) =
    ↑(aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, i))
simp [Function.uncurry, Matrix.cons_val_one, Matrix.head_cons, aeval_X]