does local increasing class instance depth break mathlib rul

Stream: maths

[Chris Hughes]

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]

Update. Proving one extra lemma has solved this problem.