simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe,
  AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X