-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem bind₁_verschiebungPoly_wittPolynomial (n : ℕ) :
    bind₁ verschiebungPoly (wittPolynomial p ℤ n) =
      if n = 0 then 0 else p * wittPolynomial p ℤ (n - 1)

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ → ℤ),
    (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
      (MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))

Tactic:
intro x

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ (MvPolynomial.eval x) (verschiebungPoly k) = (verschiebung (mk p x)).coeff k

Tactic:
simp only [← aeval_verschiebungPoly]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ (MvPolynomial.eval x) (verschiebungPoly k) = (aeval (mk p x).coeff) (verschiebungPoly k)

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ (MvPolynomial.eval x) (verschiebungPoly k) = (aeval (mk p x).coeff) (verschiebungPoly k)

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

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ ↑p * (ghostComponent n) (mk p x) = ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
rfl

Result:
no goals

Proof state:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
calc
  _ = ghostComponent (n + 1) (verschiebung <| mk p x) := by
   apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
   funext k
   simp only [← aeval_verschiebungPoly]
   exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
  _ = _ := by rw [ghostComponent_verschiebung]; rfl

Result:
no goals

Proof state:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n.succ)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n.succ - 1))

Tactic:
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]

Result:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ n)

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))

Tactic:
split_ifs with hn

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (fun i => (MvPolynomial.eval x) (verschiebungPoly i)) = (verschiebung (mk p x)).coeff

Tactic:
funext k

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ (MvPolynomial.eval x) (verschiebungPoly k) = (verschiebung (mk p x)).coeff k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)

Tactic:
apply MvPolynomial.funext

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ → ℤ),
    (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
      (MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn

Result:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n.succ)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n.succ - 1))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (ghostComponent (n + 1)) (verschiebung (mk p x)) = ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
rw [ghostComponent_verschiebung]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ ↑p * (ghostComponent n) (mk p x) = ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Proof state:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ n)

Tactic:
simp only [add_eq_zero, and_false, ite_false, map_mul]

Result:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) 0

Tactic:
simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero, ite_true]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    (ghostComponent (n + 1)) (verschiebung (mk p x))

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

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (fun i => (MvPolynomial.eval x) (verschiebungPoly i)) = (verschiebung (mk p x)).coeff

Proof state:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
rw [map_natCast, hom_bind₁]

Result:
case neg.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)