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

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivRight R S₁) (C r) = C (Polynomial.C r)
Tactic:
unfold optionEquivRight AlgEquiv.ofAlgHom
State after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : 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' := ⋯ }
      (C r) =
    C (Polynomial.C r)

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : 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' := ⋯ }
      (C r) =
    C (Polynomial.C r)
Tactic:
simp only [Option.elim, AlgEquiv.coe_mk, aeval_C]
State after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (algebraMap R (MvPolynomial S₁ (Polynomial R))) r = C (Polynomial.C r)

State before:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (algebraMap R (MvPolynomial S₁ (Polynomial R))) r = C (Polynomial.C r)
Tactic:
rfl
State after:
no goals