-- Mathlib/RingTheory/WittVector/MulP.lean
theorem bind₁_wittMulN_wittPolynomial (n k : ℕ) :
    bind₁ (wittMulN p n) (wittPolynomial p ℤ k) = n * wittPolynomial p ℤ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n k : ℕ
⊢ (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k

Tactic:
induction' n with n ih

Result:
case zero
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ (bind₁ (wittMulN p 0)) (wittPolynomial p ℤ k) = ↑0 * wittPolynomial p ℤ k

case succ
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih : (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ (bind₁ (wittMulN p (n + 1))) (wittPolynomial p ℤ k) = ↑(n + 1) * wittPolynomial p ℤ k

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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

Tactic:
simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply,
  Matrix.cons_val_zero, Matrix.head_cons, Matrix.cons_val_one]

Result:
no goals

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih : (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ (bind₁ (wittMulN p (n + 1))) (wittPolynomial p ℤ k) = ↑(n + 1) * wittPolynomial p ℤ k

Tactic:
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]

Result:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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)) =
    ↑(n + 1) * wittPolynomial p ℤ k

Proof state:
case zero
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ (bind₁ (wittMulN p 0)) (wittPolynomial p ℤ k) = ↑0 * wittPolynomial p ℤ k

Tactic:
simp [wittMulN, Nat.cast_zero, zero_mul, bind₁_zero_wittPolynomial]

Result:
no goals

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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)) =
    ↑(n + 1) * wittPolynomial p ℤ k

Tactic:
simp only [map_add, Nat.cast_succ, bind₁_X_right]

Result:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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

Tactic:
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]

Result:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
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