Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-16 13:18 ee6a9fa7

View on Github →

fix(tactic/simps): fix bug (#7433)

  • Custom projections that were compositions of multiple projections failed when the projection has additional arguments.
  • Also adds an error when two projections are given the same simps-name

Estimated changes