CategoryTheory.Aut.ext

theorem CategoryTheory.Aut.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {φ₁ φ₂ : CategoryTheory.Aut X}, φ₁.hom = φ₂.hom → φ₁ = φ₂

This theorem states that for any given category `C` and object `X` in `C`, and any two automorphisms `φ₁` and `φ₂` of `X`, if the morphisms from `X` to itself induced by `φ₁` and `φ₂` are equal, then the automorphisms `φ₁` and `φ₂` themselves are equal. In essence, it establishes that two automorphisms of an object in a category are identical if their corresponding morphisms are identical.

More concisely: If `φ₁` and `φ₂` are automorphisms of an object `X` in a category `C` such that the morphisms `X  X` induced by `φ₁` and `φ₂` are equal, then `φ₁` and `φ₂` are equal as automorphisms.