no goals
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.674878
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
⊢ LinearMap.range (toLinearPMap g hg).toFun = map (LinearMap.snd R E F) g
rw [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]