I have found that adding or removing a theorem in a set of mutually-inductive theorems can significantly affect the processing time.
For example, I had five mutually-inductive theorems. The time to compile the file was about 2 hours and 45 minutes. By modifying one definition, I was able to combine two of these into one theorem with the same proof cases. With these four mutually-inductive theorems, the time to compile the file was about 10 minutes.
In a different case, I had to modify some definitions to add a couple of cases in a proof and add a theorem to a set of mutually-inductive theorems. This changed the processing time from a few minutes to several hours.
Why does the addition or removal of a single theorem in a set of mutually-inductive theorems without other significant changes so affect the time to process a proof? Is there a way to reduce the processing time with the addition of a needed mutually-inductive theorem?