We report on challenges and solutions in making large mechanised proofs scale based on our experience proving correctness properties for a cache coherence protocol. This was a difficult proof that required hundreds of iterations to get right, and ultimately led to an inductive invariant with nearly 800 conjuncts, and to over 54,000 proof obligations. To address the challenges in proof engineering this, we developed \supersketch{}, a tool that automates the generation of proofs involving multiple subgoals in Isabelle/HOL, enabling efficient management and maintenance of large-scale proofs. We discuss the iterative development of the inductive invariant, the lack of modularity in proofs of inductive invariants, and how \supersketch{} mitigates these issues. We further contribute tools to fix corner cases that cannot be fully automated with \supersketch{}, such as correcting proof scripts invalidated by upstream definition changes. This allowed us to drop simplifying restrictions in our model whilst retaining the correctness proof, as we avoid significant manual effort inspecting and fixing the broken lines of the original proof when making the model more general. Our work provides insights into proof engineering practices and highlights the need for improved support in proof assistants for large-scale mechanized proofs.