The finite coradical filtration conjecture for co-Frobenius Hopf algebras

Let $H$ be a co-Frobenius Hopf algebra, meaning that it has a nonzero left integral (equivalently, any of the equivalent conditions characterizing co-Frobenius Hopf algebras). Its coradical filtration is the filtration $\{H_n\}_{n\geq 0}$ associated with the coradical $H_0$ of the underlying coalgebra. Finite coradical filtration conjecture. The coradical filtration of $H$ is finite: there exists $n\geq 0$ such that $H=H_n$. The conjecture was proved by the cited result of Andruskiewitsch, Cuadra, and Etingof, so the claim is now a theorem.