no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sb : Submodule R M
sc : Submodule R P
hsb : FG sb
hsc : FG sc
tb : Set M
htb : Set.Finite tb ∧ span R tb = sb
tc : Set P
htc : Set.Finite tc ∧ span R tc = sc
⊢ span R (↑(LinearMap.inl R M P) '' tb ∪ ↑(LinearMap.inr R M P) '' tc) = Submodule.prod sb sc
rw [LinearMap.span_inl_union_inr, htb.2, htc.2]