Checking equivalence of two polytopes
I cannot say for sure if you will consider the following approach as better, but from a complexity-theoretic point of view there is a more efficient solution. The idea is to rephrase your question in the first-order theory of the rationals with addition and order. You have that $P_1$ is included in $P_2$ if and only if
\begin{align*}
\Phi := 
\forall \vec{x}.\exists \vec{y}.\left( A \cdot \vec{x} \le b \implies \left( A \cdot \vec{y} \le b \wedge \bigwedge_{1\le i\le m} f_i(\vec{x}) = g_i(\vec{y}) \right)\right)
\end{align*}
is valid. It is clear how to derive equivalence of $P_1$ and $P_2$ in the same way. Now $\Phi$ has a fixed quantifier-alternation prefix, and is consequently decidable in $\Pi_2^\text{P}$, the second level of the polynomial-time hierarchy (Sontag, 1985). I'm pretty confident that it is possible to also prove a matching lower bound, I recall reading somewhere that inclusion between two polytopes is $\Pi_2^\text{P}$-hard.

If you are looking for tool support in order to solve such problems in practice, modern SMT-solvers such as z3 fully support this theory.