Commit 2026-07-15 12:13 50b6a3e8

feat: use to_dual for HeytingAlgebra (#33543) This PR adds to_dual for HeytingAlgebra, BiheytingAlgebra, GeneralizedHeytingAlgebra. There is a bit of friction around dualizing compl to hnot, because this means that theorems about compl in boolean algebras will not be able to be translated nicely with to_dual. This should not be that many theorems, so this is acceptable. See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Dualize.20sdiff.20and.20himp/with/599261487 Since we have GeneralizedCoheytingAlgebra.toDistribLattice, I removed CoheytingAlgebra.toDistribLattice. Aligning the Heyting and Coheyting API is kind of awkward, because they are unfortunately quite different. One reason is that the arguments of sup/inf are often swapped in the dual version, which is not compatible with to_dual. I've worked around this with extensive use of to_dual none. There are quite some lemmas that in my eyes seem unnecessary, such as le_sup_sdiff_sup_sdiff, but I haven't removed any in this PR.