Commit 2026-03-22 14:08 5d5ae53e

View on Github →

feat(Order/GaloisConnection/Defs): use to_dual for GaloisInsertion/GaloisCoinsertion (#35649) This PR uses to_dual to generate declarations about GaloisCoinsertion from those for GaloisInsertion.

An entry is added to the name translation dictionary for this particular name translation.
One lemma in another file had to be tagged.
Some uses of to_dual have been replaced with to_dual none, because I had written them before to_dual none existed.

Estimated changes

Modified Mathlib/Algebra/Group/Submonoid/Units.lean

Modified Mathlib/Order/GaloisConnection/Defs.lean

deleted theorem GaloisCoinsertion.l_injective

deleted theorem GaloisCoinsertion.l_le_l_iff

deleted def GaloisCoinsertion.monotoneIntro

deleted theorem GaloisCoinsertion.strictMono_l

deleted theorem GaloisCoinsertion.u_bot

deleted theorem GaloisCoinsertion.u_l_eq

deleted theorem GaloisCoinsertion.u_l_leftInverse

deleted theorem GaloisCoinsertion.u_surjective

deleted def GaloisConnection.liftOrderTop

modified theorem GaloisConnection.monotone_intro

deleted def GaloisConnection.toGaloisCoinsertion

deleted def GaloisInsertion.dual

deleted def GaloisInsertion.ofDual

Modified Mathlib/Order/Monotone/Defs.lean

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified Mathlib/Topology/Order.lean