no goals
R : Type u_3
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.694525
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ graph (inverse hf) = Submodule.map (LinearEquiv.prodComm R E F) (graph f)
rw [inverse, Submodule.toLinearPMap_graph_eq]