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

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivRight R S₁) (X (Option.some x)) = X x
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
State after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ { 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 (Option.some x)) =
    X x

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ { 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 (Option.some x)) =
    X x
Tactic:
simp only [AlgEquiv.coe_mk, aeval_X, Option.elim]
State after:
no goals