rw [<-DFunLike.congr_fun optionEquivRight_comp_to_MvPolynomial_Option p]
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) = C p
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) =
    ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) p