no goals
R : Type u
inst✝ : Ring R
G✝ H✝ : ModuleCat R
f✝ : G✝ ⟶ H✝
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ofHom (Submodule.subtype (LinearMap.range f)) = Limits.image.ι f
erw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]