Post #1471881

@xenaproject @andrejbauer p.s. for larger projects I can also imagine having a fourth "tactical" group devoted to developing relevant Lean tactics for the project. In PFR for instance we found ourselves repeatedly needing to verify that certain quantities were finite (this was an artefact of our probability theory being based on the Mathlib library for unsigned measures, which were allowed to take the value \(+\infty\)), and Heather Macbeth kindly supplied us with a useful `finiteness` tactic to resolve all these issues easily.