Commit 2025-05-01 08:12 a8f8e758
View on Github →refactor(Order/Heyting): convert toBiheytingHomClass from lemma to instance (#24437) Previously toBiheytingHomClass was a lemma due to concerns about typeclass loops. These concerns are no longer relevant in Lean 4, so we can now make it a proper instance. Remove the outdated porting note as well.