Prove by induction that for all $n$, $8$ is a factor of $7^{2n+1} +1$

Below I explain how the nonmodular inductive proofs in other answers are really just applications of modular arithmetic product rules. Indeed, let's examine closely the inductive step

$\qquad\qquad\quad\! 8\mid \overbrace{(7^{\large 2n+1}\!+1)}^{\large\rm P(n)},\quad\ 8\mid (7^{\large 2} - 1)$

$\qquad\ \ \ \Rightarrow\ \ 8\mid (7^{\large 2n+1}\!+\color{#c00}1)\,\color{#0a0}{7^{\large 2}}\color{#c00}{-1}\,(\color{#0a0}{7^{\large 2}}-1)\, =\, \smash{\overbrace{7^{\large 2n+3}-1}^{\large\rm P(n+1)}}\ \ $ is a special case of Proof below

$\begin{eqnarray} \rm {\bf Lemma}\ \ &\rm m\ \ |&\rm\ \, X\!-\!x\quad\ \& &&\rm\! m\ |\: Y\!-\!y \ \Rightarrow\ m\:|\!\!&&\rm XY - \: xy\ \ \ \, {\bf [Divisibility\ Product\ Rule]} \\[.3em] \rm {\bf Proof}\ \ \ \ \ &\rm m\ \ |&\rm (X\!-\!\color{#c00}x)\:\color{#0a0}Y\ \,+ &&\rm\, \color{#c00}x\ (\color{#0a0}Y\!-\!y)\ \ \ \ = &&\rm XY - \: xy \\[.5em] \rm {\bf Lemma}\ \ & &\rm\ \, X\equiv x\quad\ \ \& &&\rm\quad\ Y\equiv y \ \ \ \ \Rightarrow\ &&\rm XY\equiv xy \ \ \ \, {\bf [Congruence\ Product\ Rule]}\\[.3em] \rm {\bf Proof}\ \ \ \ \ &0\equiv& \rm (X\!-\!\color{#c00}x)\:\color{#0a0}Y\,\ + &&\rm\, \color{#C00}x\ (\color{#0a0}Y\!-\!y)\ \ \ \ \equiv &&\rm XY - \: xy \\ \end{eqnarray}$


If congruences are known, then we may simply quickly apply the Congruence Product Rule

$\qquad \color{#c00}{7^{\large 2n+1}\equiv -1},\ \ \color{#0a0}{7^{\large 2}\equiv 1}\,\Rightarrow\, 7^{\large 2n+3}= \color{#c00}{7^{\large 2n+1}}\color{#0a0}{ 7^{\large 2}}\equiv \color{#c00}{(-1)}\color{#0a0}{(1)}\equiv -1\pmod 8$

Thus, with the help of modular language, we see that the induction simplifies to the trivial induction that $\, a\equiv 1\,\Rightarrow\, a^n\equiv 1\,$ (here $\,\color{#0a0}{a = 7^2}).\,$ Or, $\,7\equiv -1\,\Rightarrow\, 7^n\equiv (-1)^n\equiv -1$ for odd $\,n\,$ by the Congruence Power Rule, which abstracts such iterated applications of the Product Rule.

So the nonmodular proofs can be viewed as the result of compiling the higher-level (congruence) language proofs into lower-level (divisibility) assembly language. One can do such compilation mechanically for any such congruence proof. Just as for software, the low-level assembly language is far less comprehensible since it eliminates higher level conceptual structure - which often leads to great simplification, e.g $\,a\equiv 1\,\Rightarrow\,a^n\equiv 1\,$ above.

Also worth mention is that this proof can be discovered mechanically, i.e. without any required insight, be using the method of multiplicative telescopy.


Inductive step

$$7^{(2(n+1)+1)}+1=7^{(2n+1+2)}+1=49\times\left(7^{(2n+1)}+1\right)-8\times 6$$