R : Type u
M : Type v
F : Type ?u.138961
G : Type ?u.138964
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' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
s : Set M
x : M
⊢ x ∈ span R (⋃ (s_1 : R) (_ : s_1 ∈ ↑I) (t : M) (_ : t ∈ s), {s_1 • t}) ↔
    x ∈ span R (⋃ (a : R) (_ : a ∈ I) (b : M) (_ : b ∈ s), {a • b})
R : Type u
M : Type v
F : Type ?u.138961
G : Type ?u.138964
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' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
s : Set M
x : M
⊢ x ∈ I • span R s ↔ x ∈ span R (⋃ (a : R) (_ : a ∈ I) (b : M) (_ : b ∈ s), {a • b})
rw [← I.span_eq, Submodule.span_smul_span, I.span_eq]
no goals
R : Type u
M : Type v
F : Type ?u.138961
G : Type ?u.138964
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' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
s : Set M
x : M
⊢ x ∈ span R (⋃ (s_1 : R) (_ : s_1 ∈ ↑I) (t : M) (_ : t ∈ s), {s_1 • t}) ↔
    x ∈ span R (⋃ (a : R) (_ : a ∈ I) (b : M) (_ : b ∈ s), {a • b})
rfl