$N\subseteq\ker\Phi$: the relators $i_{\alpha\beta}(\omega)\,i_{\beta\alpha}(\omega)^{-1}$ lie in the kernel

Setting and binders. Let $X$ be an arbitrary type equipped with a topology, and let $\iota$ be an arbitrary index type (no finiteness, nonemptiness, decidable-equality, or any other assumption is made on $\iota$; in particular $\iota$ may be empty). Let $A : \iota \to \mathcal{P}(X)$ be an arbitrary family of subsets $A_\alpha \subseteq X$, let $x_0 \in X$ be a point, and assume

$$h_{x_0} :\quad \forall \alpha \in \iota,\; x_0 \in A_\alpha .$$

This is the only hypothesis on the data. In particular, the statement does not assume that the $A_\alpha$ are open, that they cover $X$ (no hypothesis $\bigcup_\alpha A_\alpha = X$), that any $A_\alpha$ is path-connected, that any pairwise intersection $A_\alpha \cap A_\beta$ is path-connected, or anything about triple intersections $A_\alpha \cap A_\beta \cap A_\gamma$. Each $A_\alpha$ and each $A_\alpha \cap A_\beta$ is regarded as a topological space with the subspace topology inherited from $X$. Both $X$ and $\iota$ are implicit arguments; $A$, $x_0$, $h_{x_0}$ are explicit.

Fundamental groups (Mathlib notion). For a topological space $Y$ and a point $y \in Y$, $\pi_1(Y, y)$ denotes the group whose elements are equivalence classes of loops $[0,1] \to Y$ based at $y$, two loops being identified when they are homotopic through loops based at $y$ (homotopy relative to the endpoints). Concretely it is the endomorphism monoid of the object $y$ in the fundamental groupoid of $Y$. The identity is the class of the constant loop and the inverse is the class of the reversed loop. The multiplication convention is that of composition in the groupoid: for loop classes $p, q$ one has $p \cdot q = q \ast p$, i.e. the product $p\cdot q$ is "first traverse $q$, then traverse $p$".

Basepoints. Using $h_{x_0}$, the point $x_0$ is regarded as a point of each subspace: $\mathrm{basept}_\alpha := x_0 \in A_\alpha$ (the pair $(x_0, h_{x_0}(\alpha))$), and, for each pair $\alpha, \beta \in \iota$, $\mathrm{basept}_{\alpha\beta} := x_0 \in A_\alpha \cap A_\beta$ (the pair $(x_0, (h_{x_0}(\alpha), h_{x_0}(\beta)))$). Below I write all three fundamental groups with basepoint $x_0$, understanding these subspace points.

The inclusion-induced homomorphisms. For each $\alpha \in \iota$,

$$(\iota_\alpha)_* :\; \pi_1(A_\alpha, x_0) \longrightarrow \pi_1(X, x_0)$$

is the group homomorphism induced by the continuous inclusion $A_\alpha \hookrightarrow X$ (the map sending a point of the subspace to its underlying point of $X$): it sends the class of a loop $\gamma$ in $A_\alpha$ to the class of the same loop viewed in $X$. (Formally it is Mathlib's "map along a continuous map, then transport along an equality of basepoints"; here the basepoint equality is the reflexivity proof that the underlying point of $\mathrm{basept}_\alpha$ is $x_0$, so no nontrivial transport occurs.)

Similarly, for each pair $\alpha, \beta \in \iota$ (not required to be distinct),

$$j^{\alpha\beta}_{L} :\; \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\alpha, x_0), \qquad j^{\alpha\beta}_{R} :\; \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\beta, x_0)$$

are the homomorphisms induced by the continuous inclusions $A_\alpha \cap A_\beta \hookrightarrow A_\alpha$ and $A_\alpha \cap A_\beta \hookrightarrow A_\beta$ respectively (again with reflexivity as the basepoint equality).

The free product (Mathlib notion). Write

$$F := \mathop{\ast}_{\alpha \in \iota} \pi_1(A_\alpha, x_0)$$

for the free product (categorical coproduct of groups) of the family of fundamental groups $\pi_1(A_\alpha, x_0)$, $\alpha \in \iota$. In Mathlib it is constructed as the quotient of the free monoid on the alphabet $\{(\alpha, g) : \alpha \in \iota,\ g \in \pi_1(A_\alpha, x_0)\}$ by the congruence generated by $(\alpha, 1) \sim 1$ and $(\alpha, g)(\alpha, g') \sim (\alpha, g g')$; it is a group because each factor is a group. For each $\alpha$ there is the canonical homomorphism $\mathrm{of}_\alpha : \pi_1(A_\alpha, x_0) \to F$ sending $g$ to the class of the one-letter word $(\alpha, g)$. The free product satisfies the universal property: a family of homomorphisms $f_\alpha : \pi_1(A_\alpha, x_0) \to G$ (for all $\alpha$) corresponds to a unique homomorphism $F \to G$ whose composite with each $\mathrm{of}_\alpha$ is $f_\alpha$. If $\iota$ is empty then $F$ is the trivial group.

The homomorphism $\Phi$. $\Phi := \mathrm{vanKampenHom}(A, x_0, h_{x_0}) : F \to \pi_1(X, x_0)$ is the homomorphism obtained from the universal property applied to the family $((\iota_\alpha)_*)_{\alpha \in \iota}$; i.e. $\Phi$ is the unique group homomorphism with

$$\Phi\big(\mathrm{of}_\alpha(g)\big) = (\iota_\alpha)_*(g) \qquad \text{for all } \alpha \in \iota,\ g \in \pi_1(A_\alpha, x_0).$$

The relator set. $R := \mathrm{vanKampenRelators}(A, x_0, h_{x_0}) \subseteq F$ is the set of all elements $g \in F$ for which there exist indices $\alpha, \beta \in \iota$ and an element $\omega \in \pi_1(A_\alpha \cap A_\beta, x_0)$ such that

$$g \;=\; \mathrm{of}_\alpha\!\big(j^{\alpha\beta}_{L}(\omega)\big)\cdot \mathrm{of}_\beta\!\big(j^{\alpha\beta}_{R}(\omega)\big)^{-1}.$$

Here $\alpha$ and $\beta$ range over all pairs, including $\alpha = \beta$ (in which case the relator is $\mathrm{of}_\alpha(j_L(\omega))\,\mathrm{of}_\alpha(j_R(\omega))^{-1}$ with both maps induced by the same inclusion $A_\alpha\cap A_\alpha \hookrightarrow A_\alpha$), and both orders $(\alpha,\beta)$ and $(\beta,\alpha)$ are included. The product is in the group $F$, and $(\cdot)^{-1}$ is inversion in $F$.

The normal subgroup $N$. $N := \mathrm{vanKampenNormal}(A, x_0, h_{x_0})$ is the normal closure of $R$ in $F$ (Mathlib notion): the subgroup of $F$ generated by the set of all conjugates $c\, r\, c^{-1}$ with $r \in R$ and $c \in F$. Equivalently, it is the smallest normal subgroup of $F$ containing $R$. (The bundle also records, as a separate instance, that $N$ is normal in $F$; this is not part of the theorem's claim.)

The kernel (Mathlib notion). $\ker \Phi$ is the subgroup $\{ g \in F \mid \Phi(g) = 1 \}$ of $F$, where $1$ is the identity of $\pi_1(X, x_0)$ (the class of the constant loop at $x_0$).

The order $\le$ on subgroups (Mathlib notion). For subgroups $H, K$ of a group, $H \le K$ means that the underlying set of $H$ is contained in the underlying set of $K$: every element of $H$ is an element of $K$.

The assertion. Under exactly the hypotheses listed above (a topology on $X$, an arbitrary family $A$, a point $x_0$, and $x_0 \in A_\alpha$ for every $\alpha$), the theorem asserts

$$N \;\le\; \ker \Phi,$$

that is: every element $g$ of the normal closure $N$ of the relator set $R$ satisfies $\Phi(g) = 1$ in $\pi_1(X, x_0)$. Unfolded fully: for every $g$ in the subgroup of $\mathop{\ast}_{\alpha} \pi_1(A_\alpha, x_0)$ generated by all conjugates of elements of the form $\mathrm{of}_\alpha(j^{\alpha\beta}_L(\omega))\,\mathrm{of}_\beta(j^{\alpha\beta}_R(\omega))^{-1}$ ($\alpha, \beta \in \iota$, $\omega \in \pi_1(A_\alpha\cap A_\beta, x_0)$), the image of $g$ under the homomorphism $\Phi$ determined by $\mathrm{of}_\alpha(h) \mapsto (\iota_\alpha)_*(h)$ is the trivial loop class in $\pi_1(X, x_0)$.

The statement is a one-directional inclusion only: it does not assert $\ker \Phi \le N$, does not assert equality $N = \ker\Phi$, and says nothing about surjectivity of $\Phi$ or about an isomorphism $F/N \cong \pi_1(X, x_0)$.

Degenerate and edge cases silently included.

• $\iota = \varnothing$: the hypothesis $h_{x_0}$ is vacuous, $F$ is the trivial group, $R = \varnothing$, $N$ is trivial, and the assertion is trivially true.
• $\iota$ a singleton $\{\alpha\}$: the only relators are $\mathrm{of}_\alpha(j_L(\omega))\,\mathrm{of}_\alpha(j_R(\omega))^{-1}$ with $j_L, j_R$ both induced by $A_\alpha \cap A_\alpha \hookrightarrow A_\alpha$.
• The sets $A_\alpha$ may be arbitrary subsets (not open, not path-connected, not covering $X$); the intersections $A_\alpha \cap A_\beta$ may be arbitrary (only the point $x_0$ is guaranteed to lie in each). The hypothesis $h_{x_0}$ is satisfiable (e.g. $A_\alpha = X$ for all $\alpha$, or $A_\alpha = \{x_0\}$), so the theorem is not vacuous in general.
• Repeated indices and both orderings of $(\alpha,\beta)$ contribute relators.