elaboration replay for large inductive theorems

Stream: general

[Frederick Pu]

I have a large inductive theorem but for some reason the elaboration time scales with the size of the theorem instead of the size of each arm. https://github.com/FrederickPu/pullback/blob/main/Pullback/SSA/SSA.lean

[Frederick Pu]

by elaboration time i mean the time it takes to reelaborate when i change the proof in one of the arms