case h.e'_6.h
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝ : ι
⊢ torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
⊢ Finset.SupIndep S fun i => torsionBy R M (q i)
convert supIndep_torsionBySet_ideal (M := M) fun i hi j hj ij =>
    (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij
no goals
case h.e'_6.h
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
inst✝ : DecidableEq ι
x✝ : ι
⊢ torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})
exact (torsionBySet_span_singleton_eq (R := R) (M := M) _).symm