ι : Type u_3
R : Type u_1
S : Type ?u.436512
M : ι → Type ?u.436517
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Submodule R N
inst✝ : (i : ι) → (x : { x // x ∈ p i }) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) f = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
ι : Type u_3
R : Type u_1
S : Type ?u.436512
M : ι → Type ?u.436517
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Submodule R N
inst✝ : (i : ι) → (x : { x // x ∈ p i }) → Decidable (x ≠ 0)
x : N
⊢ x ∈ iSup p ↔ ∃ f, (sum f fun i xi => ↑xi) = x
rw [mem_iSup_iff_exists_dfinsupp]
no goals
ι : Type u_3
R : Type u_1
S : Type ?u.436512
M : ι → Type ?u.436517
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Submodule R N
inst✝ : (i : ι) → (x : { x // x ∈ p i }) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) f = x) ↔ ∃ f, (sum f fun i xi => ↑xi) = x
simp_rw [Dfinsupp.lsum_apply_apply, Dfinsupp.sumAddHom_apply,
  LinearMap.toAddMonoidHom_coe, coeSubtype]