Commit 2023-05-06 08:46 bc9db788

View on Github →

feat: cancel_denoms tactic (#3797) Ports the tactic CancelDenoms.derive and the interactive tactic cancel_denoms. This tactic is needed to make linarith handle divisions by numbers, but this PR does not involve linarith.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/CancelDenoms.lean

added theorem CancelDenoms.add_subst

added def CancelDenoms.cancelDenominatorsInType

added theorem CancelDenoms.cancel_factors_eq

added theorem CancelDenoms.cancel_factors_eq_div

added theorem CancelDenoms.cancel_factors_le

added theorem CancelDenoms.cancel_factors_lt

added def CancelDenoms.derive

added def CancelDenoms.deriveThms

added theorem CancelDenoms.derive_trans

added theorem CancelDenoms.div_subst

added def CancelDenoms.findCompLemma

added theorem CancelDenoms.mul_subst

added theorem CancelDenoms.neg_subst

added theorem CancelDenoms.sub_subst

added def CancelDenoms.synthesizeUsingNormNum

added def cancelDenominators

added def cancelDenominatorsAt

added def cancelDenominatorsTarget

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified Mathlib/Util/Qq.lean

Modified Mathlib/Util/SynthesizeUsing.lean

added def synthesizeUsing'

modified def synthesizeUsing

added def synthesizeUsingTactic'

added def synthesizeUsingTactic

Created test/cancel_denoms.lean