!4#2986 Maschke theorem

Stream: mathlib4

[Yury G. Kudryashov]

In !4#2986, I add a shortcut instance for coercion of a docs4#LinearMap to a function. Without this instance, Lean fails to generate the coercion in the new file. With this coercion, I get a linter error in LinearAlgebra.Dfinsupp: Lean can simplify some (((s : Finset _) : Set _) : Type _) to (s : Type _) in the LHS.

[Yury G. Kudryashov]

Another issue is that Lean 4 is very slow on this file but this is probably related to already known issues with typeclasses in Lean 4.

[Yury G. Kudryashov]

UPD: it compiles (at least, locally) without this instance.

[Sebastian Ullrich]

Yury G. Kudryashov said:

Another issue is that Lean 4 is very slow on this file but this is probably related to already known issues with typeclasses in Lean 4.

Please always run the file under --profile before speculating about performance bottlenecks. For example, one of the slowest files, Mathlib.GroupTheory.MonoidLocalization, is dominated by [to_additive] interpretation.

[Eric Rodriguez]

I wonder if this slowdown is related to the non-compiling of RingHoms evaluated I had earlier; maybe it's worth checking that TC doesn't go down some loop?