Proof of Lagrange's Theorem

Step 1: the three sets have a number of elements. By claim 3 of Uniqueness of the Identity Element and of Inverses in a Group the set $G$ is nonempty, and it is finite by hypothesis, so it has $n$ elements for some natural number $n=|G|$.

The subgroup $H$ is a subset of $G$ and is nonempty, since $e_G\in H$ by condition 1 of Subgroup. Hence claim 3 of Basic Properties of Finite Sets shows that $H$ has $t$ elements for some $t\in\mathbb{N}$, and $t=|H|$.

The map $q:G\to G/H$ defined by $q(a)=aH$ is surjective, because by Left Coset, Order of a Group, and Index of a Subgroup every element of $G/H$ is of the form $aH$ for some $a\in G$. Hence claim 4 of Basic Properties of Finite Sets shows that $G/H$ is finite and nonempty and has $r$ elements for some $r\in\mathbb{N}$, and $r=[G:H]$.

Step 2: the left cosets form a partition indexed by $[r]$. Let $\Phi:[r]\to G/H$ be a bijection from the initial segment $[r]$ onto $G/H$, which exists because $G/H$ has $r$ elements. For $i\in[r]$ put $B_i=\Phi(i)$; each $B_i$ is an element of $G/H$, hence a left coset of $H$ and in particular a subset of $G$.

We verify the three hypotheses of Counting a Partition into Blocks of Equal Cardinality for the set $X=G$ and the subsets $B_i$, $i\in[r]$.

Hypothesis 1. Let $x\in G$. The left coset $xH$ is an element of $G/H$, so by surjectivity of $\Phi$ there is $i\in[r]$ with $B_i=\Phi(i)=xH$. By claim 1 of Left Cosets Partition a Group and All Have the Same Cardinality we have $x\in xH=B_i$.

Hypothesis 2. Let $i,i'\in[r]$ with $i\ne i'$. Since $\Phi$ is injective by claim 1 of Injectivity, Composition, and Restriction of Bijections, we have $B_i\ne B_{i'}$. Write $B_i=aH$ and $B_{i'}=bH$ with $a,b\in G$. If $B_i\cap B_{i'}$ were nonempty, claim 3 of Left Cosets Partition a Group and All Have the Same Cardinality would give $aH=bH$, i.e. $B_i=B_{i'}$, a contradiction. Hence $B_i\cap B_{i'}=\emptyset$.

Hypothesis 3. Each $B_i$ is a left coset, say $B_i=aH$, and $H$ has $t$ elements by Step 1, so claim 4 of Left Cosets Partition a Group and All Have the Same Cardinality shows that $B_i$ has $t$ elements.

Step 3: proof of claim 1. By Counting a Partition into Blocks of Equal Cardinality, the set $G$ has $t\cdot r$ elements. Since $G$ also has $n$ elements, Uniqueness of the Number of Elements gives $n=t\cdot r$, that is

Together with the finiteness and nonemptiness of $H$ and $G/H$ established in Step 1, this proves claim 1.

Step 4: proof of claim 2. By Step 1 the index $[G:H]$ is an element of $\mathbb{N}$, and by Step 3 we have $|G|=|H|\cdot[G:H]$. Taking $c=[G:H]$ in the definition of divisibility shows that $|H|$ divides $|G|$.