simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom]
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 hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C