This is only a partial answer since I have the same question as the OP does about lines 3 and 4, however, I am presenting it to show how this could be proven.
The question is why this proof cannot be completed in three steps? That would depend on the rules that one has available which are programmed into the proof checker one is using.
For the proof checker associated with forall x one can do exactly as the OP suggests doing and get a valid proof using conditional introduction (→I) on a sequence of lines starting and ending at line 2 and discharging the assumption made on line 2:
One could also use reiteration (R) which allows one to add a line with what one has from a previous line. This makes the sequence of lines start with 2 and end with 3:
Reiteration is a derived rule based on the basic rules defined in forall x. One could avoid this derived rule and use the more basic rules. (See page 136 for a derivation of the reiteration rule.)
Here is how it would look using conjunction introduction (∧I) and conjunction elimination (∧E):
Note that this used conjunction ("and") introduction rather than disjunction ("or") introduction as in the OP's quoted example. The "Taut" rule for line 4 is not one that I think I have, or I am unaware of it.
From the perspective of the proof checker I am using I would come to the same conclusion and ask "So why write 3 and 4, which appear completely redundant?" The answer may appear somewhere in Hurley's text where the basic rules for that text are defined.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/ Wikipedia, "Fitch notation" https://en.wikipedia.org/wiki/Fitch_notation