rw [RingHom.comp_assoc]
case hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).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