V Elt coeff

theorem vElt_coeff (α κ : ℕ) (hκ : κ + 1 ≤ α) (j s : Fin (2 ^ κ)) :    (vElt α κ hκ j).val.1.coeff (2 ^ (α - κ - 1) * (s : ℕ))      = if s = j then (if (j : ℕ) = 0 then (2 : R) else 1) else 0 := by  have hα : 1 ≤ α := by omega  have hhalf : (2 : ℕ) ^ (α - 1) = 2 ^ (α - κ - 1) * 2 ^ κ := by rw [← pow_add]; congr 1; omega  have hej : 2 ^ (α - κ - 1) * (j : ℕ) < 2 ^ (α - 1) := by    rw [hhalf]; exact mul_lt_mul_of_pos_left j.isLt (by positivity)  have hes : 2 ^ (α - κ - 1) * (s : ℕ) < 2 ^ (α - 1) := by    rw [hhalf]; exact mul_lt_mul_of_pos_left s.isLt (by positivity)  have hejα : 2 ^ (α - κ - 1) * (j : ℕ) < 2 ^ α := by    have h2 : (2 : ℕ) ^ α = 2 * 2 ^ (α - 1) := by rw [← pow_succ']; congr 1; omega    omega  have hpos : (0 : ℕ) < 2 ^ (α - κ - 1) := by positivity  have heq_iff : (2 ^ (α - κ - 1) * (s : ℕ) = 2 ^ (α - κ - 1) * (j : ℕ)) ↔ s = j := by    rw [mul_right_inj' hpos.ne', Fin.val_inj]  rw [vElt_coe, Rq.add_val, CPolynomial.coeff_add, Xpow_coeff_of_lt α hejα]  by_cases hsj : s = j  · rw [if_pos (heq_iff.mpr hsj), if_pos hsj]    by_cases hj0 : (j : ℕ) = 0    · rw [hj0, Nat.mul_zero, conjAut_Xpow, Nat.zero_mul,        Xpow_coeff_of_lt α (show (0 : ℕ) < 2 ^ α from by positivity)]      have hs0 : 2 ^ (α - κ - 1) * (s : ℕ) = 0 := by        rw [show (s : ℕ) = (j : ℕ) from by rw [hsj], hj0, Nat.mul_zero]      rw [if_pos hs0, if_pos rfl]; norm_num    · rw [conjAut_Xpow_coeff_low α hα          (Nat.mul_pos hpos (Nat.pos_of_ne_zero hj0)) hej hes, _root_.add_zero, if_neg hj0]  · rw [if_neg (fun h => hsj (heq_iff.mp h)), if_neg hsj]    by_cases hj0 : (j : ℕ) = 0    · rw [hj0, Nat.mul_zero, conjAut_Xpow, Nat.zero_mul,        Xpow_coeff_of_lt α (show (0 : ℕ) < 2 ^ α from by positivity)]      have hs0 : ¬ (2 ^ (α - κ - 1) * (s : ℕ) = 0) := by        rw [Nat.mul_eq_zero, not_or]        exact ⟨hpos.ne', fun h => hsj (Fin.ext (h.trans hj0.symm))⟩      rw [if_neg hs0, _root_.add_zero]    · rw [conjAut_Xpow_coeff_low α hα          (Nat.mul_pos hpos (Nat.pos_of_ne_zero hj0)) hej hes, _root_.add_zero]