Theorem: MvPolynomial.optionEquivRight_X_none (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
State after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X none) =
    C Polynomial.X

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ { toFun := ⇑(aeval fun o => o.elim (C Polynomial.X) X),
        invFun := ⇑(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)), left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      (X none) =
    C Polynomial.X
Tactic:
simp only [AlgEquiv.coe_mk, aeval_X, Option.elim]
State after:
no goals