R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ ⊤ • span R {x} ≤ M'
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ x ∈ M'
suffices (⊤ : Ideal R) • span R ({x} : Set M) ≤ M' by
  rw [top_smul] at this
  exact this (subset_span (Set.mem_singleton x))
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ (⋃ (s_1 : R) (_ : s_1 ∈ s) (t : M) (_ : t ∈ {x}), {s_1 • t}) ⊆ ↑M'
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ ⊤ • span R {x} ≤ M'
rw [← hs, span_smul_span, span_le]
no goals
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ (⋃ (s_1 : R) (_ : s_1 ∈ s) (t : M) (_ : t ∈ {x}), {s_1 • t}) ⊆ ↑M'
simpa using H
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : span R {x} ≤ M'
⊢ x ∈ M'
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : ⊤ • span R {x} ≤ M'
⊢ x ∈ M'
rw [top_smul] at this
no goals
R : Type u
M : Type v
F : Type ?u.105735
G : Type ?u.105738
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
this : span R {x} ≤ M'
⊢ x ∈ M'
exact this (subset_span (Set.mem_singleton x))