Product with terminal object isomorphism

Stream: general

[Jack McKoen]

I have a category C with limits, which has a terminal object T. Given an object X, I'd like to show that

X ⨯ T ≅ X

(via the projection onto X). Is there some API I can take advantage of here, or will I need to prove this explicitly?

[Adam Topaz]

docs#CategoryTheory.Limits.prod.rightUnitor

[Adam Topaz]

The defn is tagged with simps, and is defined in one direction as the projection and in the other in terms of lift, so the usual approach to proving things about (co)limits in categories should work (possibly after a dsimp).

[Jack McKoen]

This is exactly what I was looking for, thanks Adam.