isomorphisms define category

Stream: Is there code for X?

[Alena Gusakov]

I'm trying to prove this statement:

Let C be a category. Show that the collection of isomorphisms in C defines a
subcategory, the maximal groupoid inside C.

I know that the definition of groupoid exists in mathlib:

class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=
(inv       : Π {X Y : obj}, (X ⟶ Y) → (Y ⟶ X))
(inv_comp' : ∀ {X Y : obj} (f : X ⟶ Y), comp (inv f) f = id Y . obviously)
(comp_inv' : ∀ {X Y : obj} (f : X ⟶ Y), comp f (inv f) = id X . obviously)

but it seems like it builds on the definition of category. I'm interested in seeing if there's a way to grab all of the isomorphisms and objects of a category C without defining the resultant structure as a groupoid, and instead proving that it forms a category directly in order to prove the above statement? Maybe by showing that it's a category_struct first, and then showing that it's a category or something like that. Or is the definition of groupoid essentially what I'm looking for?

[Yury G. Kudryashov]

category_theory/core

[Alena Gusakov]

Thanks!