-- 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_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

Tactic:
rw [Finset.sum_subset support_mk_subset, ← hμ]

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 ∈ s, ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ 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
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = 0

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 ∉ μ.support

Tactic:
rw [mem_support_iff, not_ne_iff]

Result:
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

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 = 0
⊢ (fun x xi => ↑xi) x 0 = 0

Tactic:
rfl

Result:
no goals

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 ∈ s, x ∉ μ.support → (fun x xi => ↑xi) x (μ x) = 0

Tactic:
intro x _ 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 ∉ μ.support
⊢ (fun x xi => ↑xi) x (μ x) = 0

Proof state:
case mp.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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi => ↑xi) = a
⊢ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩

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) = a

Proof state:
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

Tactic:
rw [coe_zero, ← mem_bot R]

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) ∈ ⊥

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
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals