[GOAL]
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)
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
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)
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.cast_zero, mul_zero, zero_coeff, wittMulN, AlgHom.map_zero, Pi.zero_apply]
[GOAL]
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)
[PROOFSTEP]
rw [wittMulN, Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
[GOAL]
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)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
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)
[PROOFSTEP]
ext1 ⟨b, i⟩
[GOAL]
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))
[PROOFSTEP]
fin_cases b
[GOAL]
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))
[PROOFSTEP]
simp [Function.uncurry, Matrix.cons_val_zero, ih]
[GOAL]
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))
[PROOFSTEP]
simp [Function.uncurry, Matrix.cons_val_one, Matrix.head_cons, aeval_X]
[GOAL]
p : ℕ
R✝ : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (x * ↑n).coeff = fun n_1 => ↑(aeval x.coeff) (wittMulN p n n_1)
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R✝ : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R✝
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ coeff (x * ↑n) k = ↑(aeval x.coeff) (wittMulN p n k)
[PROOFSTEP]
exact mulN_coeff n x k
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n k : ℕ
⊢ ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k : ℕ
⊢ ↑(bind₁ (wittMulN p Nat.zero)) (wittPolynomial p ℤ k) = ↑Nat.zero * wittPolynomial p ℤ k
[PROOFSTEP]
simp [wittMulN, Nat.cast_zero, zero_mul, bind₁_zero_wittPolynomial]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (wittMulN p (Nat.succ n))) (wittPolynomial p ℤ k) = ↑(Nat.succ n) * wittPolynomial p ℤ k
[PROOFSTEP]
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X]))
      (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (wittPolynomial p ℤ k)) (X 0 + X 1)) =
    ↑(Nat.succ n) * wittPolynomial p ℤ k
[PROOFSTEP]
simp only [AlgHom.map_add, Nat.cast_succ, bind₁_X_right]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X])) (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ k)) +
      ↑(bind₁ (Function.uncurry ![wittMulN p n, X])) (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ k)) =
    (↑n + 1) * wittPolynomial p ℤ k
[PROOFSTEP]
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k n : ℕ
ih : ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ ↑(bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 0)) (wittPolynomial p ℤ k) +
      ↑(bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 1)) (wittPolynomial p ℤ k) =
    ↑n * wittPolynomial p ℤ k + wittPolynomial p ℤ k
[PROOFSTEP]
simp only [ih, Function.uncurry, Function.comp, bind₁_X_left, AlgHom.id_apply, Matrix.cons_val_zero, Matrix.head_cons,
  Matrix.cons_val_one]
