no goals
k : Type u₁
G : Type u₂
R : Type ?u.1569928
inst✝¹ : Semiring k
inst✝ : Monoid G
r : kᵐᵒᵖ
x : Gᵐᵒᵖ
⊢ ↑(RingEquiv.symm MonoidAlgebra.opRingEquiv) (single x r) = op (single (unop x) (unop r))
simp