Chris Hughes (Aug 13 2018 at 20:05):
So I'm doing Sylow's theorems in lean, and one of the proofs requires me to synthesize a
fintype instance for the product of a subtype of a subtype of a finite type and a subtype of a quotient of a subtype of a finite type. This is complicated enough that the normal depth isn't good enough, but a deeper depth is good enough. Is it approved to increase the type class inference depth to deal with situations like these? The offending code is line 404 of https://github.com/dorhinj/mathlib/blob/sylow/group_theory/sylow.lean
Chris Hughes (Aug 13 2018 at 21:24):
Update. Proving one extra lemma has solved this problem.
Last updated: May 18 2021 at 08:14 UTC