-- 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 : ι
a✝ : x ∈ s
hx : x ∉ (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩).support
⊢ ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
rw [mem_support_iff, not_ne_iff] at 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
⊢ ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = 0

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

Tactic:
intro x _ 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 : x ∉ (DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩).support
⊢ ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = 0

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

Tactic:
suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)

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 ∈ s), p x

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 : ι
⊢ x ∈ μ.support → x ∈ s

Tactic:
contrapose

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 : ι
⊢ x ∉ s → x ∉ μ.support

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 ∈ s), p x

Tactic:
exact (iSup_neg hx).symm

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 : ι
⊢ x ∉ s → x ∉ μ.support

Tactic:
intro hx

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

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

Tactic:
exact hi

Result:
no goals

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) ∈ p ↑⟨i, hi⟩

Tactic:
exact coe_mem _

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
⊢ μ.support ⊆ s

Tactic:
intro x

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 : ι
⊢ x ∈ μ.support → x ∈ s

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
⊢ a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
rw [Submodule.mem_iSup_iff_exists_dfinsupp']

Result:
ι : 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
⊢ (∃ f, (f.sum fun x xi => ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = 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 ∈ s, ↑((DFinsupp.mk s fun i => ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ i)

Tactic:
exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]

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 : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi => ↑xi) x (μ x) = 0

Tactic:
rw [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 0 = 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
⊢ (μ.sum fun x xi => ↑xi) = ∑ i ∈ s, ↑((fun i => ⟨↑(μ i), ⋯⟩) i)

Tactic:
apply Finset.sum_subset

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
⊢ μ.support ⊆ s

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

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
⊢ (∃ f, (f.sum fun x xi => ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
constructor <;> rintro ⟨μ, hμ⟩

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

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