LinearAlgebra.CrossProduct simpnf linter typeclass timeouts

Stream: nightly-testing

[Ruben Van de Velde]

github mathlib4 bot said:

:cross_mark: The latest CI for Mathlib's branch#nightly-testing has failed.

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.LinearAlgebra.CrossProduct
Error: ././././Mathlib/LinearAlgebra/CrossProduct.lean:72:1: error: cross_anticomm.{u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero ((Fin 3 → R) →ₗ[R] Fin 3 → R)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ././././Mathlib/LinearAlgebra/CrossProduct.lean:80:1: error: cross_anticomm'.{u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero ((Fin 3 → R) →ₗ[R] Fin 3 → R)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ././././Mathlib/LinearAlgebra/CrossProduct.lean:85:1: error: cross_self.{u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero ((Fin 3 → R) →ₗ[R] Fin 3 → R)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ././././Mathlib/LinearAlgebra/CrossProduct.lean:93:1: error: dot_self_cross.{u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero ((Fin 3 → R) →ₗ[R] Fin 3 → R)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ././././Mathlib/LinearAlgebra/CrossProduct.lean:101:1: error: dot_cross_self.{u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero ((Fin 3 → R) →ₗ[R] Fin 3 → R)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

I'm not sure how to deal with those, except just adding nolint

[Eric Wieser]

This looks pretty damning. I've seen this behavior on some fairly complex types around CliffordAlgebra, where simp starts failing to find random typeclasses, but these seem to simple to ignore