CategoryTheory.Groupoid.vertexGroup.inv_eq_inv

theorem CategoryTheory.Groupoid.vertexGroup.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C) (γ : c ⟶ c), γ⁻¹ = CategoryTheory.inv γ

This theorem states that for any category 'C' that is a groupoid, and for any object 'c' in 'C' and morphism 'γ' from 'c' to 'c', the inverse of 'γ' in the group of endomorphisms of 'c' is equal to the inverse of 'γ' as given by the `CategoryTheory.inv` function. In other words, the group inverse of a morphism within the endomorphisms of an object in a groupoid category is equivalent to the categorical inverse of that morphism.

More concisely: For any groupoid category 'C', the group inverse of a morphism 'γ' in the endomorphisms of object 'c' equals the categorical inverse of 'γ'.