∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f : A₀.a ⟶ A₁.a)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam)
  (f_1 : A₀.a ⟶ A₁.a)
  (h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f_1) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f_1)
      CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam),
  ({ f := f, h := h } = { f := f_1, h := h_1 }) = (f = f_1)