R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBy R M (∏ i in S, q i)
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)
rw [← Module.isTorsionBySet_span_singleton_iff, Ideal.submodule_span_eq, ←
  Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf] at hM
case h.e'_8.h
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
x✝ : { x // x ∈ S }
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)
convert torsionBySet_isInternal
    (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM
no goals
case h.e'_8.h
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : Set.Pairwise (↑S) (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ (a : ι) (_ : a ∈ S), Ideal.span {q a})
x✝ : { x // x ∈ S }
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm