rw [to_MvPolynomial_Option_X]
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) (X none) = C Polynomial.X