How rigorous must my set theory proof be?

If you really wanted formal, get rid of the $\ldots$ and prove it by induction:

For $n=2$ (the minimal case) we have $A_1 \subset A_2$ and $A_2 \subset A_1$. This means $A_1 = A_2$ by definition of $=$.

Suppose we have the statement holding for $n$ sets, and take $n+1$ sets obeying the hypotheses: $A_1 \subset A_2 \subset, \ldots \subset A_{n-1} \subset A_n \subset A_{n+1}$ and $A_{n+1} \subset A_1$. As $A_n \subset A_{n+1} \subset A_1$ simple transitivity of $\subset$ gives us $A_n \subset A_1$. But then forgetting $A_{n+1}$ for a while, we have $n$ sets obeying the hypotheses, and so we are allowed to conclude $A_1 = A_n$. So $A_{n+1} \subset A_1 = A_n \subset A_{n+1}$ and we have $A_1 = A_{n+1}$ as required. This concludes the induction step.

So it holds for all $n$.

Opinion based answer.

I think you are confusing "rigor" with "write stuff using quantification symbols and other symbols rather than words".

You ask about your lemma, which is indeed nearly obvious. If I were required to prove it I'd say

To prove two sets equal I have to prove they contain the same elements. The first inclusion says that every element of $H$ is in $J$, the second says that every element of $J$ is in $H$, so done.

In set-theory the notation $A\subseteq B$ is actually an abbreviation for:$$\forall x[x\in A\implies x\in B]$$

This makes $\subseteq$ a preorder on the sets (reflexive and transitive).

Then the axiom of extensionality is the statement that this relation is also anti-symmetric: $$A\subseteq B\wedge B\subseteq A\implies A=B\tag1$$ This makes the relation $\subseteq$ a partial order.

In my view $(1)$ is not a statement that can be proved, but is a statement based on an abbreviation and an axiom.