V Elt coeff full

theorem vElt_coeff_full (α κ : ℕ) (hκ : κ + 1 ≤ α) (j : Fin (2 ^ κ)) {p : ℕ} (hp : p < 2 ^ α) :    (vElt α κ hκ j).val.1.coeff p      = if (j : ℕ) = 0 then (if p = 0 then (2 : R) else 0)        else if p = 2 ^ (α - κ - 1) * (j : ℕ) then 1             else if p = 2 ^ α - 2 ^ (α - κ - 1) * (j : ℕ) then -1 else 0 := by  have hα : 1 ≤ α := by omega  have hhalf : (2 : ℕ) ^ (α - 1) = 2 ^ (α - κ - 1) * 2 ^ κ := by rw [← pow_add]; congr 1; omega  have hd2 : (2 : ℕ) ^ α = 2 * 2 ^ (α - 1) := by rw [← pow_succ']; congr 1; omega  rw [vElt_coe, Rq.add_val, CPolynomial.coeff_add]  set e := 2 ^ (α - κ - 1) * (j : ℕ) with he_def  have hej : e < 2 ^ (α - 1) := by    rw [he_def, hhalf]; exact mul_lt_mul_of_pos_left j.isLt (by positivity)  have hejα : e < 2 ^ α := by omega  rw [Xpow_coeff_of_lt α hejα p]  by_cases hj0 : (j : ℕ) = 0  · have he0 : e = 0 := by rw [he_def, hj0, Nat.mul_zero]    rw [if_pos hj0, he0, conjAut_Xpow, Nat.zero_mul, Xpow_coeff_of_lt α (by positivity) p]    split_ifs with h <;> norm_num  · have hepos : 0 < e := by      rw [he_def]; exact Nat.mul_pos (by positivity) (Nat.pos_of_ne_zero hj0)    rw [if_neg hj0, conjAut_Xpow_eq_neg α hepos hejα, Rq.neg_val, CPolynomial.coeff_neg,      Xpow_coeff_of_lt α (by omega : 2 ^ α - e < 2 ^ α) p]    split_ifs with h1 h2 <;> first | (exfalso; omega) | ring