The set equality in the lemma you mention only holds a.s., so it's not possible to prove that $\cap_{n \ge 1} A_n^C = \emptyset$. The best you can prove is that it has probability $0$. Apart from that, your proof looks correct.
To fix the proof, you just need to conclude from the lemma that since, as you correctly point out,
$$\bigcap_{n\ge 1} A_n^C\subseteq \left\{\sum_{n \ge 1} P (A_n |\mathcal F_{n−1}) =\infty \right\},$$
then, up to a set of probability $0$, $\{A_n \ i.o.\}$ contains the set $\cap_{n\ge 1} A_n^C$. As these two sets are disjoint, this implies that $P(\cap_{n\ge 1} A_n^C)=0$.
This is the Kochen-Stone Lemma. I will state this result and a short proof for you. But first a little technical result.
Lemma: If $0\neq f\in L_2$ and $\mathbb{E}[f]\geq0$, then for any $0<\lambda<1$
$$\begin{align}
\mathbb{P}\big[f>\lambda \mathbb{E}[f]\big]\geq (1-\lambda)^2 \frac{\big(\mathbb{E}[f]\big)^2}{\mathbb{E}[|f|^2]}\tag{1}\label{anty-cheby}.
\end{align}
$$
Here is a short proof:
By Hölder's inequality
$$
\mathbb{E}[f]=\int_{\{f\leq \lambda\mathbb{E}[f]\}}f \,d\Pr+ \int_{\{ f>\lambda\mathbb{E}[f]\}} f\,d\mathbb{P} \leq \lambda\mathbb{E}[f] + \Big(\|f\|_2\sqrt{\Pr[f>\lambda\mathbb{E}[f]]}\Big).
$$
Here is the result that we will used to get the version of Corel Cantelly closer to what you described in your problem.
Lemma(Kochen-Stone) Let $\{A_n\}\subset\mathscr{F}$. If $\sum_n\mathbb{P}[A_n]=\infty$, then
$$\begin{align}
\mathbb{P}\big[\bigcap_{n\geq1}\bigcup_{k\geq n}A_k\big]\geq\limsup_n\frac{\Big(\sum^n_{k=1}\mathbb{P}[A_k]\Big)^2}{\sum^n_{k=1}\sum^n_{m=1}\mathbb{P}[A_k\cap A_m]}\tag{2}\label{ko-sto}
\end{align}
$$
Here is a Sketch of the proof:
Without loss of generality, we assume that $\mathbb{P}[A_n]>0$ for all $n$. Let $f_n=\sum^n_{k=1}\mathbb{1}_{A_k}$, $f=\sum_{n\geq1}\mathbb{1}_{A_n}$, and for any $0<\lambda<1$, define $B_{n,\lambda}=\big\{f_n>\lambda\mathbb{P}[f_n]\big\}$.
Observe that
$$
A=\bigcap_{n\geq 1}\bigcup_{k\geq n}A_k=\{f=\infty\}\supset\bigcap_{n\geq 1}\bigcup_{k\geq n}B_{k,\lambda}=B_\lambda;
$$
then, by $\eqref{anty-cheby}$, we obtain
$$
\mathbb{P}[A]\geq\mathbb{P}[B_\lambda]\geq\limsup_{n\rightarrow\infty}\mathbb{P}[B_{n,\lambda}]\geq(1-\lambda)^2\limsup_n\frac{\big(\mathbb{E}[f_n]\big)^2}{\mathbb{E}[f^2_n]}.
$$
Letting $\lambda\rightarrow1$ gives $\eqref{ko-sto}$.
Using Kochen-Stone's Lemma one can prove the following version of the reverse Borel-Cantelli Lemma
Theorem (reverse Borel-Cantelli) Suppose $\{A_n\}\subset\mathscr{F}$ is such that for any $i\neq j$, $\mathbb{P}[A_i\cap A_j]\leq\mathbb{P}[A_i]\mathbb{P}[A_j]$. If $\sum_n\mathbb{P}[A_n]=\infty$, then $\mathbb{P}\Big[\bigcap_{n\geq1}\bigcup_{k\geq n}A_k\Big]=1$.
Here is a short proof:
Denote by $A=\bigcap_{n\geq 1}\bigcup_{k\geq n}A_k$. Let $a_n=\sum^n_{k=1}\mathbb{P}[A_k]$,, $b_n=\sum_{i\neq j}\mathbb{P}[A_i]\mathbb{P}[ A_j]$, and $c_n=\sum^n_{k=1}\mathbb{P}^2[A_k]$. By Kochen--Stone's lemma we have
$$
\mathbb{P}[A]\geq\limsup_n\frac{c_n+b_n}{a_n+b_n}
$$
From $a^2_n=c_n+b_n\leq a_n+b_n$, and $a_n\nearrow\infty$, it follows that $b_n\nearrow\infty$ and $\lim_n\tfrac{c_n}{b_n}=0=\lim_n\frac{a_n}{b_n}$. Therefore, $\mathbb{P}[A]=1$.
Reference:
https://projecteuclid.org/euclid.ijm/1256059668
Best Answer
Verify that $\{A_n i.o. \} \subset \{A_n \setminus A_{n+1} i.o \} \cup B$ where $B$ is $\lim \inf A_n$ (i.e. points that belong to $A_n$ for all $n$ sufficiently large. Note that $P(B)=0$ because $P(A_n) \to 0$. Let me know if you need more details.