This polynomial has a double root at $1$ in $\mathbb{F}_2$, so the out of the box Hensel's lemma won't apply. However we can still apply a modified version by going one power of two up. In particular the double root at 1 splits into two simple roots mod 4 (at 1 and 3). Now a modified Hensel's lemma (with essentially the same proof as the usual version) gives us that these each have a unique 2-adic lift.
One thing that is different about this modified Hensel's lemma from what you are used to is that if we want to solve $f(x) \equiv 0 \ \mod 2^n$, the lifts we get will only be unique $\mod 2^{n-1}$. In particular we get that $f(x) \equiv 0 \ \mod 2^n$ has 5 solutions for all $n > 2$.
Several years ago, I directed an informal undergraduate reading course on $p$-adic numbers. We followed Neal Koblitz's book $p$-adic Numbers, $p$-adic Analysis, and Zeta-Functions (GTM volume 58). I really like the way this book presents the subject, and the students had a similar level of background to what you describe and found the book to be at an appropriate level, so it's worth considering this book if you want a written reference for the course.
Koblitz presents the $p$-adic numbers primarily through the analytic construction. The algebraic construction of the $p$-adic integers isn't explicitly introduced in those terms, but the essence of it is contained in the following theorem that Koblitz proves in chapter 1:
Theorem 2. Every equivalence class $a$ in $\mathbb{Q}_p$ for which $\lvert a \rvert_p \leq 1$ has exactly one representative Cauchy sequence of the form $\{a_i\}$ consisting of integers such that $0 \leq a_i < p^i$ and $a_i \equiv a_{i+1} \pmod{p^i}$ for all $i$.
The proof of this theorem is followed by a discussion of $p$-adic expansions. I don't think Koblitz explicitly describes this as a separate construction using the language of abstract algebra (that is, viewing these integers as elements of $\mathbb{Z}/p^i\mathbb{Z}$), but you could add it as a remark that immediately follows from that theorem and the discussion afterward.
In other words (whether or not you use this book), I would suggest using the analytic construction to prove the existence and basic properties of $p$-adic expansions of $p$-adic numbers first (and to favor the representation of $p$-adic expansions using sequences of integers rather than sequences of residue classes of integers), and only afterwards remark that in fact one could use this as an alternative algebraic construction of the $p$-adic numbers.
This is actually fairly consistent with Hensel's original motivation, which was to explore the analogy between power series in function fields (e.g. Taylor series of complex-analytic functions at a point) and power series in number fields (that is, "$p$-adic expansion of an algebraic number"), and to use this to prove theorems in algebraic number theory. The concept of a $p$-adic expansion is central. See here for some references on the history of the $p$-adic numbers.
Best Answer
You've shown that $f(a)\equiv0\pmod{2}$ for $a=1$ and $a=2$. To show that there exists some $\alpha\in\Bbb{Z}_p$ such that $f(\alpha)=0$, you can apply Hensel's lemma as you quote it in your question; it suffices to show that $f'(a)\not\equiv0\pmod{2}$ for some $a$.