R : Type u_2
M : Type u_3
N : Type ?u.759278
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_1
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ (i : ι), p i
this : (span R {m} ≤ ⨆ (i : ι), p i) → ∃ s, span R {m} ≤ ⨆ (i : ι) (_ : i ∈ s), p i
⊢ ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
R : Type u_2
M : Type u_3
N : Type ?u.759278
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_1
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ (i : ι), p i
⊢ ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
have :=
  CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
    (Submodule.singleton_span_isCompactElement m) p
R : Type u_2
M : Type u_3
N : Type ?u.759278
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_1
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ (i : ι), p i
this : (m ∈ ⨆ (i : ι), p i) → ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
⊢ ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
R : Type u_2
M : Type u_3
N : Type ?u.759278
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_1
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ (i : ι), p i
this : (span R {m} ≤ ⨆ (i : ι), p i) → ∃ s, span R {m} ≤ ⨆ (i : ι) (_ : i ∈ s), p i
⊢ ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
simp only [Submodule.span_singleton_le_iff_mem] at this
no goals
R : Type u_2
M : Type u_3
N : Type ?u.759278
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_1
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ (i : ι), p i
this : (m ∈ ⨆ (i : ι), p i) → ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
⊢ ∃ s, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i
exact this hm