case zero
p : ℕ
R : Type ?u.51070
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k : ℕ
⊢ ↑(bind₁ (wittMulN p Nat.zero)) (wittPolynomial p ℤ k) = ↑Nat.zero * wittPolynomial p ℤ k

case succ
p : ℕ
R : Type ?u.51070
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
p : ℕ
R : Type ?u.51070
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n k : ℕ
⊢ ↑(bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
induction' n with n ih
no goals
case zero
p : ℕ
R : Type ?u.51070
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
k : ℕ
⊢ ↑(bind₁ (wittMulN p Nat.zero)) (wittPolynomial p ℤ k) = ↑Nat.zero * wittPolynomial p ℤ k
simp [wittMulN, Nat.cast_zero, MulZeroClass.zero_mul, bind₁_zero_wittPolynomial]
case succ
p : ℕ
R : Type ?u.51070
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
case succ
p : ℕ
R : Type ?u.51070
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
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
case succ
p : ℕ
R : Type ?u.51070
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
case succ
p : ℕ
R : Type ?u.51070
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
simp only [AlgHom.map_add, Nat.cast_succ, bind₁_X_right]
case succ
p : ℕ
R : Type ?u.51070
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
case succ
p : ℕ
R : Type ?u.51070
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
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
no goals
case succ
p : ℕ
R : Type ?u.51070
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
simp only [ih, Function.uncurry, Function.comp, bind₁_X_left, AlgHom.id_apply,
  Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]