$\def\A{\mathcal A}\require{AMScd}$
Disclaimer 1: "Tannaka theory" is an umbrella term referring to a family of results; I might have cherry-picked a version of the theorem that is particularly easier to prove abstractly, but it does not seem different -in generality if not in spirit- from the one in [1, Thm 7.9] or [2, 2.6.1]; correct me if I'm wrong!
Disclaimer 2: I do not claim to have reinvented the wheel. :-) just curious about the reason why the technology to prove the theorem existed 6 years before its claim, and yet nobody attempted to write down a similar proof (or did someone?).
Theorem. Let $k$ be a ring, $F : \A \to mod(k)$ a $k$-linear, faithful, strong monoidal functor with domain a $k$-linear rigid monoidal category. The codomain $mod(k)$ is finitely-generated projective $k$-modules.
Then there is a bialgebra $B\in Mod(k)$ (not necessarily fin.gen) such that $\A$ is monoidally equivalent to the category of $B$-modules $Mod(B)$.
I do category theory, I'm a simple man: allow me to prove this theorem with what I know.
I can Kan extend $F$ along itself on the right: $Ran_FF : Mod(k) \to Mod(k)$ is a monad, the codensity monad of $F$.
$Ran_FF(k)$ corresponds to the $k$-module $$ \int_A \hom_k(\hom_k(k,FA),FA) = \int_A \hom_k(FA,FA) $$ i.e. to the monoid of endo-natural transformations $Nat(F,F)$ (the monoid operation is vertical composition). I claim this is the $B$ we are looking for.
I can Kan extend $F$ on the left: $Lan_FF$ is a comonad, the density comonad of $F$.
$Lan_FF(k)$ is an object of $Mod(k)$, not very far from $B$: $$ \begin{align*} Lan_FF(k) &\cong \int^A \hom_k(FA, k)\otimes FA \\ &\cong \int^A (FA)^*\otimes FA\\ &\cong \int^A (FA\otimes FA^*)^*\\ &\cong \left(\int_A FA\otimes FA^*\right)^* = B^*\\ \end{align*} $$
- "every object of $\A$ is a $B$-module" in the following sense: the universal wedge of the end $\int_A \hom_k(FA,FA)$ is made by maps $$ \epsilon_A : B \to \hom_k(FA,FA) = End(FA) $$ and this is a ring map giving $FA$ a structure of $B$-module; a morphism $\phi : A\to A'$ in $\A$ now fits in the commutative square $$ \begin{CD} B @>\epsilon_A>> \hom_k(FA,FA) \\ @V\epsilon_{A'}VV @VV(F\phi)_* V \\ \hom_k(FA',FA') @>>(F\phi)^*> \hom_k(FA,FA')\end{CD} $$ which means that for every $b\in B$, $F\phi(b.x)=b.F\phi(x)$ where $b.\_ = \epsilon(b)$; thus it is a homomorphism of $B$-modules.
I feel this is enough to define a functor $\tilde F : \A \to Mod(B)$ (just corestrict $F$) in such a way that it is an equivalence of categories; it is full and strictly surjectve on objects, and strong monoidal & fatihful by assumption. Point 4 above entails that the multiplication of $B$ given by vertical composition of natural transformation is compatible with a comultiplication on $B^*$, precisely $$ \begin{array}{c} (Nat(F,F)\otimes Nat(F,F) \to Nat(F,F))^* \\ \hline Nat(F,F)^*\otimes Nat(F,F)^* \leftarrow Nat(F,F)^* \end{array} $$ (and $B\cong B^*$ because as $B$-module it is of course 1-dimensional).
So the theorem is proved.
Question 1: am I missing something?
Question 2: If not, why this is not the standard proof of the theorem above? It is streamlined, allows for countless generalizations, and uses nothing but elementary coend calculus. And basic algebra (but this is to be expected).
[1]:Tørris Koløen Bakke, Hopf algebras and monoidal categories (2007)
[2]: Rivano, Neantro Saavedra. "Catégories tannakiennes." Bulletin de la Société Mathématique de France 100 (1972): 417-430.