∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {P : CategoryTheory.MorphismProperty T}
  [P.IsMultiplicative] (X : T) (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X)),
  autoParam (f = CategoryTheory.CategoryStruct.id X) CategoryTheory.MorphismProperty.Over.mapId._auto_1 → P f