Commit 2023-09-08 09:40 55bbc69d

chore: split Tactic.NormNum.Basic (#7002) This was accumulating a lot of different plugins. This split makes it easier to track which tactics rely on which plugins. Summary of changes:

• Tactic.NormNum.Basic has had contents split out into separate files:
  • Eq
  • Ineq
  • Inv
  • Pow
  • OfScientific
• Tactic.NormNum.CharZero has been rolled into the new Tactic.NormNum.Inv
• Tactic.NormNum.OrderedRing has been rolled into the new Tactic.NormNum.Ineq
• Tactic.NormNum imports all the new plug-in files
• Tactic.Ring only imports the norm_num plugins it needs
• CancelDenoms moved to CancelDenoms.Core with only the imports needed by the tactic
• and replaced with a new CancelDenoms that imports CancelDenoms.Core and some additional imports for plugins that are useful when using cancel_denoms
• Linarith.Preprocessing only imports CancelDenoms.Core, rather than CancelDenoms
• add imports to Linarith that are not needed for the implementation, but make it more powerful
• SimpleGraph.Density requires an additional import because it has been removed earlier.
• test/GCongr/inequalities.lean needs the OfScientific plugin.