[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ coeff (verschiebungFun x) n = if n = 0 then 0 else coeff x (n - 1)
[PROOFSTEP]
simp only [verschiebungFun, ge_iff_le]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ coeff (verschiebungFun x) 0 = 0
[PROOFSTEP]
rw [verschiebungFun_coeff, if_pos rfl]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ ↑(ghostComponent 0) (verschiebungFun x) = 0
[PROOFSTEP]
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton, verschiebungFun_coeff_zero,
  pow_zero, pow_zero, pow_one, one_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent (n + 1)) (verschiebungFun x) = ↑p * ↑(ghostComponent n) x
[PROOFSTEP]
simp only [ghostComponent_apply, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ (Finset.sum (Finset.range (n + 1 + 1)) fun i => ↑p ^ i * coeff (verschiebungFun x) i ^ p ^ (n + 1 - i)) =
    ↑p * Finset.sum (Finset.range (n + 1)) fun i => ↑p ^ i * coeff x i ^ p ^ (n - i)
[PROOFSTEP]
rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl, zero_pow (pow_pos hp.1.pos _), mul_zero, add_zero,
  Finset.mul_sum, Finset.sum_congr rfl]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ Finset.range (n + 1) →
      ↑p ^ (x_1 + 1) * coeff (verschiebungFun x) (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
        ↑p * (↑p ^ x_1 * coeff x x_1 ^ p ^ (n - x_1))
[PROOFSTEP]
rintro i -
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * coeff (verschiebungFun x) (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * coeff x i ^ p ^ (n - i))
[PROOFSTEP]
simp only [pow_succ, mul_assoc, verschiebungFun_coeff, if_neg (Nat.succ_ne_zero i), Nat.succ_sub_succ, tsub_zero]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (verschiebungPoly n) = coeff (verschiebungFun x) n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ ↑(aeval x.coeff) (verschiebungPoly Nat.zero) = coeff (verschiebungFun x) Nat.zero
[PROOFSTEP]
simp only [verschiebungPoly, Nat.zero_eq, ge_iff_le, tsub_eq_zero_of_le, ite_true, map_zero, verschiebungFun_coeff_zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (verschiebungPoly (Nat.succ n)) = coeff (verschiebungFun x) (Nat.succ n)
[PROOFSTEP]
rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X, Nat.succ_eq_add_one,
  add_tsub_cancel_right]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsPoly p fun R _Rcr => verschiebungFun
[PROOFSTEP]
use verschiebungPoly
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type ?u.111740⦄ [inst : CommRing R] (x : 𝕎 R),
    (verschiebungFun x).coeff = fun n => ↑(aeval x.coeff) (verschiebungPoly n)
[PROOFSTEP]
simp only [aeval_verschiebung_poly', eq_self_iff_true, forall₃_true_iff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ verschiebungFun 0 = 0
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (verschiebungFun 0) Nat.zero = coeff 0 Nat.zero
[PROOFSTEP]
rw [verschiebungFun_coeff]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (verschiebungFun 0) (Nat.succ n✝) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
rw [verschiebungFun_coeff]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ (if Nat.zero = 0 then 0 else coeff 0 (Nat.zero - 1)) = coeff 0 Nat.zero
[PROOFSTEP]
simp only [if_true, eq_self_iff_true, zero_coeff, ite_self]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (if Nat.succ n✝ = 0 then 0 else coeff 0 (Nat.succ n✝ - 1)) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
simp only [if_true, eq_self_iff_true, zero_coeff, ite_self]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } (x + y) =
      ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } x +
        ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } y
[PROOFSTEP]
dsimp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R), verschiebungFun (x + y) = verschiebungFun x + verschiebungFun y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n) (verschiebungFun (x✝ + y✝)) = ↑(ghostComponent n) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refine_3.zero
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ↑(ghostComponent Nat.zero) (verschiebungFun (x✝ + y✝)) =
    ↑(ghostComponent Nat.zero) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
case refine_3.succ
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
n✝ : ℕ
⊢ ↑(ghostComponent (Nat.succ n✝)) (verschiebungFun (x✝ + y✝)) =
    ↑(ghostComponent (Nat.succ n✝)) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
⊢ ↑(map f) (↑verschiebung x) = ↑verschiebung (↑(map f) x)
[PROOFSTEP]
ext ⟨-, -⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
⊢ coeff (↑(map f) (↑verschiebung x)) Nat.zero = coeff (↑verschiebung (↑(map f) x)) Nat.zero
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑(map f) (↑verschiebung x)) (Nat.succ n✝) = coeff (↑verschiebung (↑(map f) x)) (Nat.succ n✝)
[PROOFSTEP]
exact f.map_zero
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑(map f) (↑verschiebung x)) (Nat.succ n✝) = coeff (↑verschiebung (↑(map f) x)) (Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)
[PROOFSTEP]
apply MvPolynomial.funext
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ∀ (x : ℕ → ℤ),
    ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
      ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
intro x
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero, ite_true]
[GOAL]
case neg
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (Nat.succ n))) =
    ↑(MvPolynomial.eval x) (if Nat.succ n = 0 then 0 else ↑p * wittPolynomial p ℤ (Nat.succ n - 1))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑(MvPolynomial.eval x) (if n + 1 = 0 then 0 else ↑p * wittPolynomial p ℤ n)
[PROOFSTEP]
simp only [add_eq_zero, and_false, ite_false, map_mul]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑(MvPolynomial.eval x) ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rw [map_natCast, hom_bind₁]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
calc
  _ = ghostComponent (n + 1) (verschiebung <| mk p x) :=
    by
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    simp only [← aeval_verschiebungPoly, coeff_mk]
    funext k
    exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
  _ = _ := by rw [ghostComponent_verschiebung]; rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑(ghostComponent (n + 1)) (↑verschiebung (mk p x))
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ (fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i)) = fun n => coeff (↑verschiebung (mk p x)) n
[PROOFSTEP]
simp only [← aeval_verschiebungPoly, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ (fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i)) = fun n => ↑(aeval x) (verschiebungPoly n)
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
k : ℕ
⊢ ↑(MvPolynomial.eval x) (verschiebungPoly k) = ↑(aeval x) (verschiebungPoly k)
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(ghostComponent (n + 1)) (↑verschiebung (mk p x)) = ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rw [ghostComponent_verschiebung]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑p * ↑(ghostComponent n) (mk p x) = ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rfl
