Commit 2026-03-22 03:27 2b31a89e

fix(Simps): don't reduce the type of the equality (#36656) This PR fixes a small problem with simps, that the type in the generated equality lemmas is unnecessarily reduced. This can result in raw projections, which we typically don't want in our lemmas. This doesn't affect how these lemmas behave in simp. This problem confused to_dual a bit in CategoryTheory.Iso. This PR lets us remove the respectTansparency option there.