perf: remove the mergeWithGrind linter

[chenson2018]

Having the mergeWithGrind linter on by default causes two issues:

• for performance, it means running each call to grind in duplicate
• for maintainability, it requires many small changes in the nightly-testing branch

This linting is useful, but should be reinstated on a cron basis as Mathlib does.

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 85bbc2c against b7c4fa0 are in! @chenson2018

Major changes (1)

• build//instructions changed by -47.3% (✅).

[chenson2018]

As I expected, the performance benefit is concentrated in the lambda calculus files and is highly significant.