no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P✝ Q✝ : Submodule R A
m n : A
P Q : Submodule R A
x : A
hx : x ∈ P * Q
⊢ x ∈ span R (↑P * ↑Q)
rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx