docstring

Author: fweth

Mathlib/CategoryTheory/Subobject/Basic.lean

@@ -186,7 +186,8 @@ noncomputable def arrow {X : C} (Y : Subobject X) : (Y : C) ⟶ X :=
 instance arrow_mono {X : C} (Y : Subobject X) : Mono Y.arrow :=
   (representative.obj Y).property
 
-def isoFromEq {A : C} {X Y : Subobject A} (h : X = Y) :=
+/-- Equal subobjects induce isomorphic underlying objects. -/
+def isoFromEq {A : C} {X Y : Subobject A} (h : X = Y) : underlying.obj X ≅ underlying.obj Y :=
   eqToIso (congr_arg (fun X : Subobject A => (X : C)) h)
 
 @[simp]