case inl
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 = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)

case inr
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
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 = ⊤
inst✝ : DecidableEq ι
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
cases' S.eq_empty_or_nonempty with h h
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)

case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i) ≤ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
case inr
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
apply le_antisymm
case inl
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 = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ (⨆ (i : ι) (_ : i ∈ ∅), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ ∅), p i)
case inl
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 = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
simp only [h]
no goals
case inl
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 = ⊤
inst✝ : DecidableEq ι
h : S = ∅
⊢ (⨆ (i : ι) (_ : i ∈ ∅), torsionBySet R M ↑(p i)) = torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ ∅), p i)
convert iSup_emptyset (f := fun i => torsionBySet R M (p i)) <;> simp
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ ∀ (i : ι), (⨆ (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ (⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
apply iSup_le _
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ (⨆ (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ ∀ (i : ι), (⨆ (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
intro i
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ i ∈ S → torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ (⨆ (_ : i ∈ S), torsionBySet R M ↑(p i)) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
apply iSup_le _
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
⊢ i ∈ S → torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
intro is
case st
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ ↑(⨅ (i : ι) (_ : i ∈ S), p i) ⊆ ↑(p i)
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
apply torsionBySet_le_torsionBySet_of_subset
no goals
case st
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
i : ι
is : i ∈ S
⊢ ↑(⨅ (i : ι) (_ : i ∈ S), p i) ⊆ ↑(p i)
exact (iInf_le (fun i => ⨅ _ : i ∈ S, p i) i).trans (iInf_le _ is)
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ x ∈ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
⊢ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i) ≤ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
intro x hx
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ x ∈ ⨆ (i : ι) (_ : i ∈ S), torsionBySet R M ↑(p i)
rw [mem_iSup_finset_iff_exists_sum]
case inr.a.intro
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
case inr.a
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
obtain ⟨μ, hμ⟩ :=
  (mem_iSup_finset_iff_exists_sum _ _).mp
    ((Ideal.eq_top_iff_one _).mp <| (Ideal.iSup_iInf_eq_top_iff_pairwise h _).mpr hp)
case inr.a.intro.refine'_1
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ↑(μ i) • x ∈ torsionBySet R M ↑(p i)

case inr.a.intro.refine'_2
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∑ i in S, ↑((fun i => { val := ↑(μ i) • x, property := (_ : ↑(μ i) • x ∈ torsionBySet R M ↑(p i)) }) i) = x
case inr.a.intro
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∃ μ, ∑ i in S, ↑(μ i) = x
refine' ⟨fun i => ⟨(μ i : R) • x, _⟩, _⟩
case inr.a.intro.refine'_1
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0
case inr.a.intro.refine'_1
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ↑(μ i) • x ∈ torsionBySet R M ↑(p i)
rw [mem_torsionBySet_iff] at hx⊢
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ↑{ val := a, property := ha } • ↑(μ i) • x = 0
case inr.a.intro.refine'_1
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0
rintro ⟨a, ha⟩
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ↑{ val := a, property := ha } • ↑(μ i) • x = 0
rw [smul_smul]
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
this : a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0

case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0
suffices : a * μ i ∈ ⨅ i ∈ S, p i
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
case inr.a.intro.refine'_1.mk
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
this : a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
⊢ (↑{ val := a, property := ha } * ↑(μ i)) • x = 0

case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
exact hx ⟨_, this⟩
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ (i : ι) (_ : i ∈ S), p i
rw [mem_iInf]
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ a * ↑(μ i) ∈ ⨅ (_ : j ∈ S), p j
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1
intro j
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ a * ↑(μ i) ∈ ⨅ (_ : j ∈ S), p j
rw [mem_iInf]
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
⊢ a * ↑(μ i) ∈ p j
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j
intro hj
case pos
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j

case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * ↑(μ i) ∈ p j
case this
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
⊢ a * ↑(μ i) ∈ p j
by_cases ij : j = i
case pos
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i
case pos
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j
rw [ij]
no goals
case pos
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i
exact Ideal.mul_mem_right _ _ ha
case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j
⊢ a * ↑(μ i) ∈ p j
case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * ↑(μ i) ∈ p j
have := coe_mem (μ i)
case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ∀ (i_1 : ι), i_1 ∈ S → i_1 ≠ i → ↑(μ i) ∈ p i_1
⊢ a * ↑(μ i) ∈ p j
case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j
⊢ a * ↑(μ i) ∈ p j
simp only [mem_iInf] at this
no goals
case neg
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : ∀ (a : ↑↑(⨅ (i : ι) (_ : i ∈ S), p i)), ↑a • x = 0
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ∀ (i_1 : ι), i_1 ∈ S → i_1 ≠ i → ↑(μ i) ∈ p i_1
⊢ a * ↑(μ i) ∈ p j
exact Ideal.mul_mem_left _ _ (this j hj ij)
case inr.a.intro.refine'_2
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∑ x_1 in S, ↑(μ x_1) • x = x
case inr.a.intro.refine'_2
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∑ i in S, ↑((fun i => { val := ↑(μ i) • x, property := (_ : ↑(μ i) • x ∈ torsionBySet R M ↑(p i)) }) i) = x
simp_rw [coe_mk]
no goals
case inr.a.intro.refine'_2
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 = ⊤
inst✝ : DecidableEq ι
h : Finset.Nonempty S
x : M
hx : x ∈ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ S), p i)
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ S) (_ : j ≠ i), p j }
hμ : ∑ i in S, ↑(μ i) = 1
⊢ ∑ x_1 in S, ↑(μ x_1) • x = x
rw [← Finset.sum_smul, hμ, one_smul]