-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mem_iSup_finset_iff_exists_sum {s : Finset ι} (p : ι → Submodule R N) (a : N) :
    (a ∈ ⨆ i ∈ s, p i) ↔ ∃ μ : ∀ i, p i, (∑ i ∈ s, (μ i : N)) = a

Proof state:
case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ ⨆ (_ : ↑⟨i, hi⟩ ∈ s), p ↑⟨i, hi⟩

Tactic:
rw [iSup_pos]

Result:
case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ p ↑⟨i, hi⟩

case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑⟨i, hi⟩ ∈ s

Proof state:
case mpr.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∃ f, (f.sum fun x xi => ↑xi) = a

Tactic:
refine ⟨DFinsupp.mk s ?_, ?_⟩

Result:
case mpr.intro.refine_1
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ (i : ↑↑s) → ↥(⨆ (_ : ↑i ∈ s), p ↑i)

case mpr.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ((DFinsupp.mk s ?mpr.intro.refine_1).sum fun x xi => ↑xi) = a

Proof state:
case mpr.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ((DFinsupp.mk s fun i => Subtype.casesOn i fun i hi => ⟨↑(μ i), ⋯⟩).sum fun x xi => ↑xi) = a

Tactic:
simp only [DFinsupp.sum]

Result:
case mpr.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩).support, ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = a

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
hx : x ∈ s
⊢ ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = ↑(μ x)

Tactic:
rw [mk_of_mem hx]

Result:
no goals

Proof state:
case h.h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
x : ι
hx : x ∉ s
⊢ μ x = 0

Tactic:
ext

Result:
case h.h.a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
x : ι
hx : x ∉ s
⊢ ↑(μ x) = ↑0

Proof state:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i => ⟨↑(μ i), ⋯⟩) i) = a

Tactic:
rw [← hμ]

Result:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i => ⟨↑(μ i), ⋯⟩) i) = μ.sum fun x xi => ↑xi

Proof state:
case mpr.intro.refine_1
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ (i : ↑↑s) → ↥(⨆ (_ : ↑i ∈ s), p ↑i)

Tactic:
rintro ⟨i, hi⟩

Result:
case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↥(⨆ (_ : ↑⟨i, hi⟩ ∈ s), p ↑⟨i, hi⟩)

Proof state:
case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↥(⨆ (_ : ↑⟨i, hi⟩ ∈ s), p ↑⟨i, hi⟩)

Tactic:
refine ⟨μ i, ?_⟩

Result:
case mpr.intro.refine_1.mk
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ ⨆ (_ : ↑⟨i, hi⟩ ∈ s), p ↑⟨i, hi⟩

Proof state:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i => ⟨↑(μ i), ⋯⟩) i) = μ.sum fun x xi => ↑xi

Tactic:
symm

Result:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
⊢ (μ.sum fun x xi => ↑xi) = ∑ i ∈ s, ↑((fun i => ⟨↑(μ i), ⋯⟩) i)

Proof state:
case mpr.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
rw [hx]

Result:
case mpr.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑0 = 0

Proof state:
case h.hf
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : x ∉ μ.support
⊢ (fun x xi => ↑xi) x (μ x) = 0

Tactic:
rw [mem_support_iff, not_ne_iff] at hx

Result:
case h.hf
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi => ↑xi) x (μ x) = 0