-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSup_eq_range_dfinsupp_lsum (p : ι → Submodule R N) :
    iSup p = LinearMap.range (DFinsupp.lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype)

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p ≤ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

Tactic:
apply iSup_le _

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ∀ (i : ι), p i ≤ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p = LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

Tactic:
apply le_antisymm

Result:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p ≤ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ LinearMap.range ((lsum ℕ) fun i => (p i).subtype) ≤ iSup p

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ y_1, (sumAddHom fun i => (p i).subtype.toAddMonoidHom) y_1 = y

Tactic:
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Result:
no goals

Proof state:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
v : Π₀ (i : ι), ↥(p i)
⊢ ((lsum ℕ) fun i => (p i).subtype) v ∈ iSup p

Tactic:
exact dfinsupp_sumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2

Result:
no goals

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ LinearMap.range ((lsum ℕ) fun i => (p i).subtype) ≤ iSup p

Tactic:
rintro x ⟨v, rfl⟩

Result:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
v : Π₀ (i : ι), ↥(p i)
⊢ ((lsum ℕ) fun i => (p i).subtype) v ∈ iSup p

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ y ∈ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

Tactic:
simp only [LinearMap.mem_range, lsum_apply_apply]

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ y_1, (sumAddHom fun i => (p i).subtype.toAddMonoidHom) y_1 = y

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ∀ (i : ι), p i ≤ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)

Tactic:
intro i y hy

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ y ∈ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)