R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.701262
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ Submodule.map (LinearMap.fst R F E) (Submodule.map (LinearEquiv.prodComm R E F) (graph f)) =
    Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) (graph f))
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.701262
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ (inverse hf).domain = LinearMap.range f.toFun
rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
  ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
no goals
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.701262
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ Submodule.map (LinearMap.fst R F E) (Submodule.map (LinearEquiv.prodComm R E F) (graph f)) =
    Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) (graph f))
rfl