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
⊢ IsTorsionBySet R M s ↔ IsTorsionBySet R M ↑(Ideal.span s)
rw [isTorsionBySet_iff_torsionBySet_eq_top, isTorsionBySet_iff_torsionBySet_eq_top,
  torsionBySet_eq_torsionBySet_span]