chore(CategoryTheory/Category): address some porting notes (#16095)

Author: dagurtomas

Mathlib/CategoryTheory/Category/Pairwise.lean

@@ -109,15 +109,11 @@ def diagramMap : ∀ {o₁ o₂ : Pairwise ι} (_ : o₁ ⟶ o₂), diagramObj U
   | _, _, left _ _ => homOfLE inf_le_left
   | _, _, right _ _ => homOfLE inf_le_right
 
--- Porting note: the fields map_id and map_comp were filled by hand, as generating them by `aesop`
--- causes a PANIC.
 /-- Given a function `U : ι → α` for `[SemilatticeInf α]`, we obtain a functor `Pairwise ι ⥤ α`,
 sending `single i` to `U i` and `pair i j` to `U i ⊓ U j`,
 and the morphisms to the obvious inequalities.
 -/
--- Porting note: We want `@[simps]` here, but this causes a PANIC in the linter.
--- (Which, worryingly, does not cause a linter failure!)
--- @[simps]
+@[simps]
 def diagram : Pairwise ι ⥤ α where
   obj := diagramObj U
   map := diagramMap U

Mathlib/CategoryTheory/Category/PartialFun.lean

@@ -46,8 +46,6 @@ instance : CoeSort PartialFun Type* :=
 def of : Type* → PartialFun :=
   id
 
--- Porting note: removed this lemma which is useless because of the expansion of coercions
-
 instance : Inhabited PartialFun :=
   ⟨Type*⟩
 

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -85,14 +85,7 @@ theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
 @[nolint defLemma, inherit_doc leOfHom]
 abbrev _root_.Quiver.Hom.le := @leOfHom
 
--- Porting note: why does this lemma exist? With proof irrelevance, we don't need to simplify proofs
--- @[simp]
-theorem leOfHom_homOfLE {x y : X} (h : x ≤ y) : h.hom.le = h :=
-  rfl
-
--- Porting note: linter gives: "Left-hand side does not simplify, when using the simp lemma on
--- itself. This usually means that it will never apply." removing simp? It doesn't fire
--- @[simp]
+@[simp]
 theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
   rfl