p : ℕ
R S : Type u
σ : Type ?u.696083
idx : Type ?u.696086
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ + y✝).coeff = fun n => peval (wittAdd p n) ![x✝.coeff, y✝.coeff]
p : ℕ
R S : Type u
σ : Type ?u.696083
idx : Type ?u.696086
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (x + y).coeff = fun n => peval (wittAdd p n) ![x.coeff, y.coeff]
intros
case h
p : ℕ
R S : Type u
σ : Type ?u.696083
idx : Type ?u.696086
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ coeff (x✝¹ + y✝) x✝ = peval (wittAdd p x✝) ![x✝¹.coeff, y✝.coeff]
p : ℕ
R S : Type u
σ : Type ?u.696083
idx : Type ?u.696086
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ + y✝).coeff = fun n => peval (wittAdd p n) ![x✝.coeff, y✝.coeff]
ext
no goals
case h
p : ℕ
R S : Type u
σ : Type ?u.696083
idx : Type ?u.696086
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ coeff (x✝¹ + y✝) x✝ = peval (wittAdd p x✝) ![x✝¹.coeff, y✝.coeff]
exact add_coeff _ _ _