apply Polynomial.hom_congr_vars
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V) = C
case hC
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C

case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X