unfold optionEquivRight AlgEquiv.ofAlgHom
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X
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