ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ f, (sum f fun i xi => ↑xi) = a) ↔ ∃ μ, ∑ i in s, ↑(μ i) = a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (a ∈ ⨆ (i : ι) (_ : i ∈ s), p i) ↔ ∃ μ, ∑ i in s, ↑(μ i) = a
rw [Submodule.mem_iSup_iff_exists_dfinsupp']
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∃ μ, ∑ i in s, ↑(μ i) = a

case mpr.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∃ f, (sum f fun i xi => ↑xi) = a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ f, (sum f fun i xi => ↑xi) = a) ↔ ∃ μ, ∑ i in s, ↑(μ i) = a
constructor <;> rintro ⟨μ, hμ⟩
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i) = a
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∃ μ, ∑ i in s, ↑(μ i) = a
use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i) = sum μ fun i xi => ↑xi
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i) = a
rw [← hμ]
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ (sum μ fun i xi => ↑xi) = ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i)
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i) = sum μ fun i xi => ↑xi
symm
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ support μ ⊆ s

case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∀ (x : ι), x ∈ s → ¬x ∈ support μ → (fun i xi => ↑xi) x (↑μ x) = 0
case mp.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ (sum μ fun i xi => ↑xi) = ∑ i in s, ↑((fun i => { val := ↑(↑μ i), property := (_ : ↑(↑μ i) ∈ p i) }) i)
apply Finset.sum_subset
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
⊢ x ∈ support μ → x ∈ s
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ support μ ⊆ s
intro x
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
⊢ ¬x ∈ s → ¬x ∈ support μ
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
⊢ x ∈ support μ → x ∈ s
contrapose
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ¬x ∈ support μ
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
⊢ ¬x ∈ s → ¬x ∈ support μ
intro hx
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑μ x = 0
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ¬x ∈ support μ
rw [mem_support_iff, not_ne_iff]
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑(↑μ x) = ↑0
case mp.intro.h
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑μ x = 0
ext
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑(↑μ x) ∈ ⊥
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑(↑μ x) = ↑0
rw [coe_zero, ← mem_bot R]
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
this : ⊥ = ⨆ (_ : x ∈ s), p x
⊢ ↑(↑μ x) ∈ ⊥

case this
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ⊥ = ⨆ (_ : x ∈ s), p x
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ↑(↑μ x) ∈ ⊥
suffices : ⊥ = ⨆ (_ : x ∈ s), p x
no goals
case this
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
⊢ ⊥ = ⨆ (_ : x ∈ s), p x
exact (iSup_neg hx).symm
no goals
case mp.intro.h.a
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
hx : ¬x ∈ s
this : ⊥ = ⨆ (_ : x ∈ s), p x
⊢ ↑(↑μ x) ∈ ⊥
exact this.symm ▸ coe_mem (μ x)
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ¬x ∈ support μ
⊢ (fun i xi => ↑xi) x (↑μ x) = 0
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
⊢ ∀ (x : ι), x ∈ s → ¬x ∈ support μ → (fun i xi => ↑xi) x (↑μ x) = 0
intro x _ hx
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ↑μ x = 0
⊢ (fun i xi => ↑xi) x (↑μ x) = 0
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ¬x ∈ support μ
⊢ (fun i xi => ↑xi) x (↑μ x) = 0
rw [mem_support_iff, not_ne_iff] at hx
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ↑μ x = 0
⊢ (fun i xi => ↑xi) x 0 = 0
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ↑μ x = 0
⊢ (fun i xi => ↑xi) x (↑μ x) = 0
rw [hx]
no goals
case mp.intro.hf
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), { x // x ∈ ⨆ (_ : i ∈ s), p i }
hμ : (sum μ fun i xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : ↑μ x = 0
⊢ (fun i xi => ↑xi) x 0 = 0
rfl
case mpr.intro.refine'_1
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ (i : ↑↑s) → { x // x ∈ ⨆ (_ : ↑i ∈ s), p ↑i }

case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ (sum (Dfinsupp.mk s ?mpr.intro.refine'_1) fun i xi => ↑xi) = a
case mpr.intro
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∃ f, (sum f fun i xi => ↑xi) = a
refine' ⟨Dfinsupp.mk s _, _⟩
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∑ x in
      support
        (Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                    p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }),
      ↑(↑(Dfinsupp.mk s fun i =>
              { val := ↑(μ ↑i),
                property :=
                  (_ :
                    ↑(μ ↑i) ∈
                      ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                        p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
          x) =
    a
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ (sum
      (Dfinsupp.mk s fun i =>
        Subtype.casesOn i fun i hi =>
          { val := ↑(μ i),
            property := (_ : ↑(μ i) ∈ ⨆ (_ : ↑{ val := i, property := hi } ∈ s), p ↑{ val := i, property := hi }) })
      fun i xi => ↑xi) =
    a
simp only [Dfinsupp.sum]
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∑ x in s,
      ↑(↑(Dfinsupp.mk s fun i =>
              { val := ↑(μ ↑i),
                property :=
                  (_ :
                    ↑(μ ↑i) ∈
                      ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                        p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
          x) =
    ∑ i in s, ↑(μ i)

case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∀ (x : ι),
    x ∈ s →
      ¬x ∈
            support
              (Dfinsupp.mk s fun i =>
                { val := ↑(μ ↑i),
                  property :=
                    (_ :
                      ↑(μ ↑i) ∈
                        ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                          p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }) →
        ↑(↑(Dfinsupp.mk s fun i =>
                  { val := ↑(μ ↑i),
                    property :=
                      (_ :
                        ↑(μ ↑i) ∈
                          ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                            p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
              x) =
          0
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∑ x in
      support
        (Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                    p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }),
      ↑(↑(Dfinsupp.mk s fun i =>
              { val := ↑(μ ↑i),
                property :=
                  (_ :
                    ↑(μ ↑i) ∈
                      ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                        p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
          x) =
    a
rw [Finset.sum_subset support_mk_subset, ← hμ]
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∀ (x : ι),
    x ∈ s →
      ¬x ∈
            support
              (Dfinsupp.mk s fun i =>
                { val := ↑(μ ↑i),
                  property :=
                    (_ :
                      ↑(μ ↑i) ∈
                        ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                          p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }) →
        ↑(↑(Dfinsupp.mk s fun i =>
                  { val := ↑(μ ↑i),
                    property :=
                      (_ :
                        ↑(μ ↑i) ∈
                          ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                            p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
              x) =
          0
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∑ x in s,
      ↑(↑(Dfinsupp.mk s fun i =>
              { val := ↑(μ ↑i),
                property :=
                  (_ :
                    ↑(μ ↑i) ∈
                      ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                        p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
          x) =
    ∑ i in s, ↑(μ i)

case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∀ (x : ι),
    x ∈ s →
      ¬x ∈
            support
              (Dfinsupp.mk s fun i =>
                { val := ↑(μ ↑i),
                  property :=
                    (_ :
                      ↑(μ ↑i) ∈
                        ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                          p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }) →
        ↑(↑(Dfinsupp.mk s fun i =>
                  { val := ↑(μ ↑i),
                    property :=
                      (_ :
                        ↑(μ ↑i) ∈
                          ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                            p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
              x) =
          0
exact Finset.sum_congr rfl fun x hx => congr_arg Subtype.val <| mk_of_mem hx
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ { x // x ∈ ⨆ (_ : ↑{ val := i, property := hi } ∈ s), p ↑{ val := i, property := hi } }
case mpr.intro.refine'_1
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ (i : ↑↑s) → { x // x ∈ ⨆ (_ : ↑i ∈ s), p ↑i }
rintro ⟨i, hi⟩
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ ⨆ (_ : ↑{ val := i, property := hi } ∈ s), p ↑{ val := i, property := hi }
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ { x // x ∈ ⨆ (_ : ↑{ val := i, property := hi } ∈ s), p ↑{ val := i, property := hi } }
refine' ⟨μ i, _⟩
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ p ↑{ val := i, property := hi }

case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑{ val := i, property := hi } ∈ s
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ ⨆ (_ : ↑{ val := i, property := hi } ∈ s), p ↑{ val := i, property := hi }
rw [iSup_pos]
no goals
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ p ↑{ val := i, property := hi }
exact coe_mem _
no goals
case mpr.intro.refine'_1.mk
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑{ val := i, property := hi } ∈ s
exact hi
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ¬x ∈
      support
        (Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
⊢ ↑(↑(Dfinsupp.mk s fun i =>
            { val := ↑(μ ↑i),
              property :=
                (_ :
                  ↑(μ ↑i) ∈
                    ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                      p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
        x) =
    0
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
⊢ ∀ (x : ι),
    x ∈ s →
      ¬x ∈
            support
              (Dfinsupp.mk s fun i =>
                { val := ↑(μ ↑i),
                  property :=
                    (_ :
                      ↑(μ ↑i) ∈
                        ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                          p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) }) →
        ↑(↑(Dfinsupp.mk s fun i =>
                  { val := ↑(μ ↑i),
                    property :=
                      (_ :
                        ↑(μ ↑i) ∈
                          ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                            p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
              x) =
          0
intro x _ hx
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ↑(Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
      x =
    0
⊢ ↑(↑(Dfinsupp.mk s fun i =>
            { val := ↑(μ ↑i),
              property :=
                (_ :
                  ↑(μ ↑i) ∈
                    ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                      p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
        x) =
    0
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ¬x ∈
      support
        (Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
⊢ ↑(↑(Dfinsupp.mk s fun i =>
            { val := ↑(μ ↑i),
              property :=
                (_ :
                  ↑(μ ↑i) ∈
                    ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                      p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
        x) =
    0
rw [mem_support_iff, not_ne_iff] at hx
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ↑(Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
      x =
    0
⊢ ↑0 = 0
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ↑(Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
      x =
    0
⊢ ↑(↑(Dfinsupp.mk s fun i =>
            { val := ↑(μ ↑i),
              property :=
                (_ :
                  ↑(μ ↑i) ∈
                    ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s),
                      p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
        x) =
    0
rw [hx]
no goals
case mpr.intro.refine'_2
ι : Type u_1
R : Type u_2
S : Type ?u.457456
M : ι → Type ?u.457461
N : Type u_3
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → { x // x ∈ p i }
hμ : ∑ i in s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx :
  ↑(Dfinsupp.mk s fun i =>
          { val := ↑(μ ↑i),
            property :=
              (_ :
                ↑(μ ↑i) ∈
                  ⨆ (_ : ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) } ∈ s), p ↑{ val := ↑i, property := (_ : ↑i ∈ ↑s) }) })
      x =
    0
⊢ ↑0 = 0
rfl