As a starting note, the rules are syntax-directed: there's only one rule for each language construct. This means that you can construct the typing proof from the bottom up, by always using the rule for the syntactic construct at the bottom of the program. The only uncertainty is what types to use. To do the type inference manually, use variables where you don't know what a type should be, and replace a variable by a type expression (which may itself contain other variables) throughout the derivation when you reach a point where you do know something about that variable. (This is called doing unification during type inference.)
The expression $\mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f$ cannot be typed in the simply-typed lambda calculus since the two occurrences of $f$ need to have different types. It's a typical example of a program that requires polymorphism. This tells you that you'll need to make use of polymorphism: you'll need to apply the (T-Var') rule for the two occurrences of $f$ with different types, and you'll need to apply the (T-Let') rule in a way that allows using $f$ with different types.
When you write “$\lambda x. x$ is of type $\alpha\to\alpha$”, keep in mind that $\alpha$ is a variable which must be bound somewhere. In Hindley-Milner terminology, a variable in an environment has a type scheme. $\lambda x. x$ has the type scheme $\forall \alpha. \alpha\to\alpha$. You could choose to give it other type schemes, but this one is the most general (it's called the principal type scheme of the expression): all other type schemes $\tau$ for $\lambda x. x$ satisfy $\tau \sqsubseteq \forall \alpha. \alpha\to\alpha$.
The application of the (T-Let') rule that gives $\lambda x. x$ its most general type scheme is
$$
\dfrac{\vdash \lambda x.x : \alpha\to\alpha \qquad
f: \forall \alpha. \alpha\to\alpha \vdash f \, f : \color{blue}{\tau'}}
{\vdash \mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f : \color{blue}{\tau'}}
\textsf{(T-Let')}
$$
for some type $\tau'$. To find $\tau'$, find a type derivation for the second premise. The expression is an application, so you have to apply the (T-App) rule.
$$
\dfrac{f: \forall \alpha. \alpha\to\alpha \vdash f : \color{green}{\tau} \to \color{blue}{\tau'} \qquad
f: \forall \alpha. \alpha\to\alpha \vdash f : \color{blue}{\tau'}}
{f: \forall \alpha. \alpha\to\alpha \vdash f \, f : \color{blue}{\tau'}}
\textsf{(T-App)}
$$
Each premise is a variable so you need to apply the (T-Var') rule. The first premise tells you that whatever $\color{green}{\tau}$ and $\color{blue}{\tau'}$ are, they must be equal, since $\color{green}{\tau} \to \color{blue}{\tau'} \sqsubseteq \forall \alpha. \alpha\to\alpha$. The second premise tells you that $\color{blue}{\tau'}$ must have the form $\color{red}{\tau''} \to \color{orange}{\tau'''}$, since $\color{blue}{\tau'} \sqsubseteq \forall \alpha. \alpha\to\alpha$. You thus have the derivation
$$
\dfrac{\dfrac{\vdots}{\vdash \lambda x.x : \alpha\to\alpha} \qquad
\dfrac{\dfrac{}{\Gamma_1 \vdash f : \color{red}{\tau''} \to \color{orange}{\tau'''} \to \color{red}{\tau''} \to \color{orange}{\tau'''}} \qquad
\dfrac{}
{\Gamma_1 \vdash f : \color{red}{\tau''} \to \color{orange}{\tau'''}}}
{\Gamma_1 \vdash f \, f : \color{red}{\tau''} \to \color{orange}{\tau'''}}}
{\vdash \mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f : \color{red}{\tau''} \to \color{orange}{\tau'''}}
$$
where $\Gamma_1 = f: \forall \alpha. \alpha\to\alpha$ and $\color{red}{\tau''}$ and $\color{orange}{\tau'''}$ can be any types.