A group pushout is the quotient of a free product by the amalgamating relations

Given: The objects and hypotheses in the statement.

Given homomorphisms $f:K\to G$ and $h:K\to H$ as in def-group-homomorphism, a pushout is a group $P$ with homomorphisms $i_G:G\to P$ and $i_H:H\to P$ such that $i_G\circ f=i_H\circ h$, and such that every compatible pair $u:G\to Q$, $v:H\to Q$ factors through a unique $w:P\to Q$ with $w\circ i_G=u$ and $w\circ i_H=v$. The maps $f,h$ need not be injective. (Pushouts of group homomorphisms).

For a family $(G_i)_{i\in I}$, a free product is a group $F$ with homomorphisms $\iota_i:G_i\to F$ in the sense of def-group-homomorphism, such that for every group $H$ and every family of homomorphisms $f_i:G_i\to H$, there is a unique homomorphism $f:F\to H$ satisfying $f\circ\iota_i=f_i$ for all $i$. It is denoted $\ast_{i\in I}G_i$. Injectivity of the maps $\iota_i$ is not part of this definition. (The free product of an arbitrary family of groups).

Let $G$ be a group and let $S\subseteq G$. The family $\mathcal N_S:=\{N:N\mathrel{\trianglelefteq}G\text{ and }S\subseteq N\}$ is nonempty because $G\mathrel{\trianglelefteq}G$ by def-normal-subgroup. Its intersection is normal by lem-intersection-of-normal-subgroups. The normal closure of $S$ in $G$ is $\langle\!\langle S\rangle\!\rangle_G:=\bigcap_{N\in\mathcal N_S}N.$ It contains $S$ and is contained in every normal subgroup of $G$ that contains $S$. Thus it is the smallest normal subgroup of $G$ containing $S$. (The normal closure of a subset of a group).

Let $G$ be a group and let $N\mathrel{\trianglelefteq}G$ be a normal subgroup (def-normal-subgroup). The quotient group, or factor group, $G/N$ has the left cosets $G/N:=\{gN:g\in G\}$ as its elements (def-coset, def-index), with product $(gN)(hN):=ghN.$ Independence of the chosen representatives is proved in thm-coset-multiplication-well-defined-iff-normal, and the group axioms are proved in thm-quotient-group-laws. (The quotient group $G/N$ and coset product $(gN)(hN)=ghN$).

A homomorphism that kills a normal subgroup factors uniquely through the quotient group. If $N\mathrel{\trianglelefteq}G$, $f:G\to H$ is a homomorphism, and $N\subseteq\ker f$, then there is a unique homomorphism $\bar f:G/N\to H$ such that $\bar f(gN)=f(g)$ and $f=\bar f\circ\pi$. (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Let $G$ be a group and $R\subseteq G$. Then $\langle\!\langle R\rangle\!\rangle_G=\left\{g_1r_1^{\varepsilon_1}g_1^{-1}\cdots g_nr_n^{\varepsilon_n}g_n^{-1}:n\in\mathbb N,\ g_i\in G,\ r_i\in R,\ \varepsilon_i\in\{1,-1\}\right\}.$ For $n=0$ the displayed product is the identity. Replacing every conjugator $g_i$ by $g_i^{-1}$ gives the equivalent convention $g_i^{-1}r_i^{\varepsilon_i}g_i$. (The normal closure of $R$ is the set of finite products of conjugates of elements of $R$ and their inverses).