no goals
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ IsTorsionBy R M a ↔ torsionBy R M a = ⊤
rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
  isTorsionBySet_iff_torsionBySet_eq_top]