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

State before:
F V : Type
inst✝ : Field F
⊢ (to_MvPolynomial_Option V) Polynomial.X = X none
Tactic:
simp [to_MvPolynomial_Option]
State after:
no goals