Commit 2026-03-06 20:54 5fa1909e

View on Github →

chore(Tactic/CancelDenoms/Core): namespace in Mathlib.Tactic (#36177) This PR properly namespaces the cancel_denoms tactic. This is needed to stop library search from suggesting lemmas internal to this tactic.

Estimated changes

Modified Mathlib/Tactic/CancelDenoms/Core.lean

deleted structure CancelDenoms.CancelResult

deleted theorem CancelDenoms.add_subst

deleted def CancelDenoms.cancelDenominatorsInType

deleted theorem CancelDenoms.cancel_factors_eq

deleted theorem CancelDenoms.cancel_factors_eq_div

deleted theorem CancelDenoms.cancel_factors_le

deleted theorem CancelDenoms.cancel_factors_lt

deleted theorem CancelDenoms.cancel_factors_ne

deleted def CancelDenoms.derive

deleted def CancelDenoms.deriveThms

deleted theorem CancelDenoms.derive_trans

deleted theorem CancelDenoms.derive_trans₂

deleted theorem CancelDenoms.div_subst

deleted def CancelDenoms.findCompLemma

deleted theorem CancelDenoms.inv_subst

deleted theorem CancelDenoms.mul_subst

deleted theorem CancelDenoms.neg_subst

deleted theorem CancelDenoms.pow_subst

deleted theorem CancelDenoms.sub_subst

deleted def CancelDenoms.synthesizeUsingNormNum

added structure Mathlib.Tactic.CancelDenoms.CancelResult

added theorem Mathlib.Tactic.CancelDenoms.add_subst

added def Mathlib.Tactic.CancelDenoms.cancelDenominatorsInType

added theorem Mathlib.Tactic.CancelDenoms.cancel_factors_eq

added theorem Mathlib.Tactic.CancelDenoms.cancel_factors_eq_div

added theorem Mathlib.Tactic.CancelDenoms.cancel_factors_le

added theorem Mathlib.Tactic.CancelDenoms.cancel_factors_lt

added theorem Mathlib.Tactic.CancelDenoms.cancel_factors_ne

added def Mathlib.Tactic.CancelDenoms.derive

added def Mathlib.Tactic.CancelDenoms.deriveThms

added theorem Mathlib.Tactic.CancelDenoms.derive_trans

added theorem Mathlib.Tactic.CancelDenoms.derive_trans₂

added theorem Mathlib.Tactic.CancelDenoms.div_subst

added def Mathlib.Tactic.CancelDenoms.findCompLemma

added theorem Mathlib.Tactic.CancelDenoms.inv_subst

added theorem Mathlib.Tactic.CancelDenoms.mul_subst

added theorem Mathlib.Tactic.CancelDenoms.neg_subst

added theorem Mathlib.Tactic.CancelDenoms.pow_subst

added theorem Mathlib.Tactic.CancelDenoms.sub_subst

deleted def cancelDenominators

deleted def cancelDenominatorsAt

deleted def cancelDenominatorsTarget

Modified scripts/nolints.json