Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$

Given: A finite group $G$ and a subgroup $H\le G$.

The distinct left cosets of $H$ partition $G$ (The left cosets of a subgroup partition the group).

The subgroup, every coset, and $G/H$ are finite; every coset has cardinality $|H|$ and $|G/H|=[G:H]$ (In a finite group, the subgroup, every coset and the set of cosets are finite, Every left or right coset of $H$ is equinumerous with $H$, The coset set $G/H$ and the index $[G:H]$ of a subgroup).

For a finite partition $A=\bigsqcup_{i\in I}A_i$, one has $|A|=\sum_{i\in I}|A_i|$; if every summand has the same value $c$, then $\sum_{i\in I}c=|I|c$ (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition, The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form).

The order $|G|$ of a finite group is the unique natural equinumerous with its underlying set, hence agrees with finite cardinality (The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity, The cardinality $\lvert A\rvert$ of a finite set).

The embedding $\iota$ preserves multiplication, and $d\mid a$ in $\mathbb Z$ means $a=dq$ for some integer $q$ (The naturals embed in the integers, Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$).