Unfolding Category Theory definitions

Stream: new members

[VayusElytra]

Hi, I've been having some trouble lately with unfolding category theory definitions in Lean. Here's an MWE of a frequent difficulty I have:

open CategoryTheory

lemma SomeCatLemma (C : Type) [Category C] {h : C = C} :
  𝟙 C = eqToHom h := by
  rw [eqToHom]

This results in the following tactic state:
image.png

where the dots stand for eqToHom.proof_1 h : (C ⟶ C) = (C ⟶ C).
Of course, in this toy example, it's not a big deal, and just using simp suffices to prove the goal anyway, but in more complex proofs, even simp starts producing these .mpr lines that I am not sure what to do with. How should one deal with this?

[Andrew Yang]

eqToHom should not be unfolded. You should use the API of it to manipulate it to the form eqToHom (_ : X = X) and use docs#CategoryTheory.eqToHom_refl

[VayusElytra]

I guess this MWE is a little too M to see, but this also happens when working with my own category theory definitions, which makes using simp and the like necessary to even build the API I'd need.

[Bbbbbbbbba]

Maybe you can just ignore those .mpr lines (e.g. rfl already works here)?