Theorem: optionEquivRight_to_MvPolynomial_Option (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
F V : Type
inst✝ : Field F
p : Polynomial F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) p) = C p
Tactic:
rw [<-DFunLike.congr_fun optionEquivRight_comp_to_MvPolynomial_Option p]
State after:
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

State before:
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
Tactic:
simp
State after:
no goals