Commit 2026-09-28 05:55 0c51c7e4
View on Github →chore: remove some backward.isDefEq.respectTransparency.instanceSearchTypes (#44157)
This PR removes some of the recently introduced backward.isDefEq.respectTransparency.instanceSearchTypes options, using a simple fix.
In some cases the problematic lemma has been removed entirely because it was added as a simp normal form variant of another lemma, but that other lemma is already in simp normal form.
By the way, each of these has a long AI explanation of the failure that is not super helpful.