chore(Order/Hom/WithTopBot): use to_dual (leanprover-community#37274)

Use `to_dual` on `WithBot`/`WithTop` morphism definitions. This removes one `backward.isDefEq.respectTransparency` option.

Intentionally remove `simps!` from `LatticeHom.withTopWithBot` and `LatticeHom.withTop'`, instead putting `simp` on the equivalent manual lemma`.

Author: JovanGerb