p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (-x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R),
    (-x).coeff = fun n => ↑(aeval x.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
intros
case h
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (-x✝) n = ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (-x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
funext n
case h
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = ↑(eval₂Hom (algebraMap ℤ R✝) (x✝.coeff ∘ Prod.snd)) (wittNeg p n)
case h
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (-x✝) n = ↑(aeval x✝.coeff) ((fun n => ↑(rename Prod.snd) (wittNeg p n)) n)
rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ uncurry ![x✝.coeff] = x✝.coeff ∘ Prod.snd
case h
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = ↑(eval₂Hom (algebraMap ℤ R✝) (x✝.coeff ∘ Prod.snd)) (wittNeg p n)
apply eval₂Hom_congr rfl _ rfl
case h.mk
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 1
k : ℕ
⊢ uncurry ![x✝.coeff] (i, k) = (x✝.coeff ∘ Prod.snd) (i, k)
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ uncurry ![x✝.coeff] = x✝.coeff ∘ Prod.snd
ext ⟨i, k⟩
case h.mk.head
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ uncurry ![x✝.coeff] ({ val := 0, isLt := (_ : 0 < 1) }, k) =
    (x✝.coeff ∘ Prod.snd) ({ val := 0, isLt := (_ : 0 < 1) }, k)
case h.mk
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 1
k : ℕ
⊢ uncurry ![x✝.coeff] (i, k) = (x✝.coeff ∘ Prod.snd) (i, k)
fin_cases i
no goals
case h.mk.head
p : ℕ
R S : Type u
σ : Type ?u.633934
idx : Type ?u.633937
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ uncurry ![x✝.coeff] ({ val := 0, isLt := (_ : 0 < 1) }, k) =
    (x✝.coeff ∘ Prod.snd) ({ val := 0, isLt := (_ : 0 < 1) }, k)
rfl