no goals
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : FG N₁
hN₂ : FG N₂
t₁ : Set M
ht₁ : Set.Finite t₁ ∧ span R t₁ = N₁
t₂ : Set M
ht₂ : Set.Finite t₂ ∧ span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂
rw [span_union, ht₁.2, ht₂.2]