Commit 2026-04-05 08:48 c8b8884d

View on Github →

chore(Order/Hom/WithTopBot): use to_dual (#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`.

Estimated changes

deleted def InfHom.withBot'
deleted theorem InfHom.withBot_comp
deleted theorem InfHom.withBot_id
deleted def InfHom.withTop'
deleted theorem InfHom.withTop_comp
deleted theorem InfHom.withTop_id
deleted theorem LatticeHom.coe_withBot
deleted theorem LatticeHom.withBot_apply
deleted theorem LatticeHom.withBot_comp
deleted theorem LatticeHom.withBot_id
deleted def WithBot.coeOrderHom