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