-- Mathlib/LinearAlgebra/DFinsupp.lean
lemma mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
    x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Proof state:
case intro.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
i : ι
hi : i ∈ f.support
⊢ (fun x xi => ↑xi) i ((DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩) i) = (fun _i xi => xi) i (f i)

Tactic:
simp [Finsupp.mem_support_iff.mp hi]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
x✝ : ∃ f, (f.sum fun x xi => ↑xi) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum fun x xi => ↑xi) = x
⊢ ∀ (a : ι), a ∈ f.support ↔ (fun i => ↑(f i)) a ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.refine_1.h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
a✝ : ι
⊢ a✝ ∈ (DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩).support ↔ a✝ ∈ f.support

Tactic:
simp [mk_eq_zero]

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ ∃ f_1, (f_1.sum fun x xi => ↑xi) = f.sum fun _i xi => xi

Tactic:
refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩

Result:
case intro.intro.refine_1
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ (DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩).support = f.support

case intro.intro.refine_2
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
i : ι
hi : i ∈ f.support
⊢ (fun x xi => ↑xi) i ((DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩) i) = (fun _i xi => xi) i (f i)

Proof state:
case intro.intro.refine_1
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ (DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩).support = f.support

Tactic:
ext

Result:
case intro.intro.refine_1.h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
a✝ : ι
⊢ a✝ ∈ (DFinsupp.mk f.support fun i => ⟨f ↑i, ⋯⟩).support ↔ a✝ ∈ f.support

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
x✝ : ∃ f, (f.sum fun x xi => ↑xi) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum fun x xi => ↑xi) = x
⊢ ∀ (i : ι), { support := f.support, toFun := fun i => ↑(f i), mem_support_toFun := ⋯ } i ∈ p i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x

Tactic:
rw [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
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi => ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x) → ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
rintro ⟨f, hf, rfl⟩

Result:
case intro.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ ∃ f_1, (f_1.sum fun x xi => ↑xi) = f.sum fun _i xi => xi

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi => ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x

Tactic:
refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x) → ∃ f, (f.sum fun x xi => ↑xi) = x