feat(order/heyting_algebra): Heyting algebras

[YaelDillies]

Define (generalized) Heyting, co-Heyting and bi-Heyting algebras.

---

• [x] depends on: #15302
• [x] depends on: #15304
• [x] depends on: #15340

This a second go at #5527.

I made up generalized_coheyting_algebra as the intersection of generalized_boolean_algebra and coheyting_algebra, and generalized_heyting_algebra as the dual of the previous. Without generalized_coheyting_algebra, I would need to duplicate 25 lemmas between generalized_boolean_algebra and coheyting_algebra.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15302~~
• ~~leanprover-community/mathlib#15304~~
• ~~leanprover-community/mathlib#15340~~ By Dependent Issues (🤖). Happy coding!

[b-mehta]

Is this WIP or ready for review? It looks like some parts don't compile and the linter fails. Also, I think this would be easier to review if the different parts were split up - to my eyes it seems that there are unrelated changes to boolean algebras, as well as heyting, coheyting and biheyting algebras

[YaelDillies]

(I was still fixing post-merge)

It's not obvious to split that PR, as all the changes I did are required to insert biheyting algebras under boolean algebras in the order hierarchy (and making two arguments explicit to two lemmas, which was not strictly required). In particular:

• I delete all the lemmas that are now generalized to coheyting algebras.
• I prime the lemmas that are now generalized to coheyting algebras but required to prove that boolean algebras are coheyting algebras.
• I move lemmas that are neither generalized nor required for boolean_algebra → coheyting_algebra after the instance (so that they can use the generalized lemmas).

I see two ways to make a nicer diff:

• Do not generalize the lemmas to coheyting algebras. This means starting with a very poor API for coheyting algebras (and probably heyting algebras too as it would be weird to have a lemma without its dual), and the followup PR won't have a much smaller diff. I would rather not.
• Put everything in order.heyting_algebra in a temporary namespace, and remove that namespace along with the now duplicated lemmas in a followup PR. This is reducing the diff for the sake of reducing the diff, as the two PRs will be mostly disjoint, but I'm happy to do it if you ask. This is what I did in the division_monoid saga (#14000).

[b-mehta]

(assigning to Anne as the three of us discussed offline)

[Vierkantor]

Could you list the following things in the PR description:

• Declarations that have been renamed
• Declarations that have been changed (ignoring generalization of instance parameters, e.g. boolean_algebra to heyting_algebra)
• (Optionally:) Declarations that have been changed (including instance parameters)

Not only will that make it this PR easier to review, it also should make it easier to fix breaking dependencies.

[YaelDillies]

I have listed what you asked :)

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests