case a
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSup p ≤ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))

case a
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i)) ≤ iSup p
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSup p = LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
apply le_antisymm
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ ∀ (i : ι), p i ≤ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
case a
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSup p ≤ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
apply iSup_le _
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ y ∈ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ ∀ (i : ι), p i ≤ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
intro i y hy
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ y_1, ↑(sumAddHom fun i => LinearMap.toAddMonoidHom (Submodule.subtype (p i))) y_1 = y
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ y ∈ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i))
simp only [LinearMap.mem_range, lsum_apply_apply]
no goals
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
y : N
hy : y ∈ p i
⊢ ∃ y_1, ↑(sumAddHom fun i => LinearMap.toAddMonoidHom (Submodule.subtype (p i))) y_1 = y
exact ⟨Dfinsupp.single i ⟨y, hy⟩, Dfinsupp.sumAddHom_single _ _ _⟩
case a.intro
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ p i }
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) v ∈ iSup p
case a
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ LinearMap.range (↑(lsum ℕ) fun i => Submodule.subtype (p i)) ≤ iSup p
rintro x ⟨v, rfl⟩
no goals
case a.intro
ι : Type u_3
R : Type u_1
S : Type ?u.348674
M : ι → Type ?u.348679
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ p i }
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) v ∈ iSup p
exact dfinsupp_sumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2