no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑↑ₐ r)
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)