no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a
simp only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub,
  isUnit_smul_iff]