Can we collect (or maybe even write) tutorials and guides on doing analysis in various Proof Assistants? Community wiki style?
I was reading Lawrence Paulson's blog (highly recommend!) the other week and https://lawrencecpaulson.github.io/2021/11/17/Cauchy-Schwarz-example.html in particular. It employs pretty specific rules, tactics and theorems relevant to calculus.
I have an impression analysis-formalizing libraries for other proof assistants develop some specific tactics and notations too. For instance I looked over https://github.com/math-comp/analysis/ and https://github.com/lecopivo/SciLean
So the question is: where can I learn about that specifics?
For Program Analysis we have very comprehensive guides like Software Foundations, PLFA, Concrete Semantics and Functional Algorithms, Verified (plus their "fan translations" from one Proof Assistant to another). Do we have (or can we have) anything comparable for Mathematical Analysis?
A related but narrower question was mostly misunderstood and poorly answered as far as I can tell (but decided to mention for completeness).