How to match on value from Category.Over.OverMorphism?

Stream: lean4

[Joey Eremondi]

I'm wondering, what is the "right" way to deconstruct an over-category morphism? Say we've got X Y : Over Z and f : X ⟶ Y, how can we decompose it into some Category.Over.homMk (f' : X.left ⟶ Y.left) (pf : f' ≫ Y.hom = X.hom )?

I know I can get those fields with the accessors, but what about when f occurs in my goal and I want the goal and hypotheses rewritten?

Directly matching on it gives a CommaMorphism, which means that all of the lemmas about over categories require a ton of rewriting.

[Yaël Dillies]

(Can someone move this to #mathlib4 ?)

[Markus Himmel]

For CostructuredArrow, there are docs#CategoryTheory.CostructuredArrow.eq_mk and docs#CategoryTheory.CostructuredArrow.eta but it appears that no one has specialized them to Over yet. Note though that in my experience trying to destruct morphisms in comma categories can easily lead you into DTT hell, so there might be a better way to achieve your goal (see #xy)

[Joey Eremondi]

@Markus Himmel Yes I am absolutely currently in DTT hell, I'm about to start another thread asking about how to resolve that. Thanks.

[Joey Eremondi]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/DTT.20hell.3A.20How.20to.20debug.20when.20equal.20things.20aren't.20equal.3F