no goals
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ↑(opRingEquiv R) (op (↑(monomial n) r)) = ↑(monomial n) (op r)
simp only [opRingEquiv, RingEquiv.coe_trans, Function.comp_apply,
  AddMonoidAlgebra.opRingEquiv_apply, RingEquiv.op_apply_apply, toFinsuppIso_apply, unop_op,
  toFinsupp_monomial, Finsupp.mapRange_single, toFinsuppIso_symm_apply, ofFinsupp_single]