Commit 2024-02-12 10:30 0796b060

chore(Tactic/{Positivity,NormNum}): remove support for non-canonical spellings (#10344) Mul.mul or Nat.mul etc should not ever appear in a goal, so there is little reason for these tactics to support them. If these are in your goal, then something has already gone wrong and norm_num isn't responsible for saving you; that's simp or dsimp's job. Zulip thread