I did search on the site already and while there are questions that reference, for example, PLFA for Agda, there doesn't seem to be a canonical list of references for people just learning about proof assistants. I am looking at Isabelle/HOL: A Proof Assistant for Higher-Order Logic and Reasoning about Functional Programs - Sparkle: a Proof Assistant for Clean at the moment, but it would be nice to have some guidance as well.
I have experience with Haskell and functional programming, as well as more with C, and I'm coming to this from the direction of wondering how useful this might be in Banach Space Theory where much of the reasoning is built on well-structured normed linear spaces. So ideally I'm looking for references that describe using proof assistants with Functional Analysis and Banach Space Theory, preferably with a discussion of dual spaces and the interplay between Banach and dual spaces.
However, as the question was originally asked with less focus and obtained answers then as well, to not invalidate them, I will also accept references to books that present a strong learning path in other mathematical areas from which it is clear how to transfer the learning over to a new area (like Functional Analysis). I know proof assistants already handle linear algebra quite well, so my interest largely lies in taking that the further step to the linear functional case.