no goals
p : ℕ
R✝ : Type ?u.636245
S : Type ?u.636248
T : Type ?u.636251
hp : Fact (Nat.Prime p)
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.636266
β : Type ?u.636269
x y : 𝕎 R✝
R : Type u_1
i : Fin 0
j : ℕ
⊢ coeff ![] j = ![]
rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩