Commit 2026-04-08 16:40 5b08395f

View on Github →

chore: remove unneeded to_dual existing (#37778) Not exhaustive, just a few that I came across.

Estimated changes

Modified Mathlib/Order/Cover.lean

deleted theorem CovBy.Ioc_eq

deleted theorem CovBy.Ioo_eq_Ioc

Modified Mathlib/Order/Hom/Basic.lean

deleted theorem OrderIso.toRelIsoGT_symm

Modified Mathlib/Order/UpperLower/Basic.lean

deleted theorem IsLowerSet.preimage

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified Mathlib/Topology/Order/SuccPred.lean

deleted theorem PredOrder.isOpen_singleton_of_not_isPredPrelimit