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 ι
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBy R M (q i)) = ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
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 ι
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBy R M (q i)) = torsionBy R M (∏ i in S, q i)
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
  Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
  iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
case e_s
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 ι
⊢ (fun i => ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i => ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
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 ι
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBy R M (q i)) = ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
congr
case e_s.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✝ : ι
⊢ (⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝)) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
case e_s
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 ι
⊢ (fun i => ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i => ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
ext : 1
case e_s.h.e_s
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✝ : ι
⊢ (fun h => torsionBy R M (q x✝)) = fun h => torsionBySet R M ↑(Ideal.span {q x✝})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
case e_s.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✝ : ι
⊢ (⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝)) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
congr
case e_s.h.e_s.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✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
case e_s.h.e_s
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✝ : ι
⊢ (fun h => torsionBy R M (q x✝)) = fun h => torsionBySet R M ↑(Ideal.span {q x✝})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
ext : 1
case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
case e_s.h.e_s.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✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})

case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
exact (torsionBySet_span_singleton_eq _).symm
no goals
case hp
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 ι
⊢ Set.Pairwise ↑S fun i j => Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)