Proof of Lagrange's Theorem

Routine facts about inclusions and disjoint classes are used without comment (Toolkit for AL1).

By Left Cosets Partition a Group and All Have the Same Cardinality (iv), $G/H$ is the quotient of $G$ by an equivalence relation, so the canonical projection is a surjective function from $G$ onto $G/H$ (Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (vi)). Since $G$ is finite, $G/H$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi); this is the first assertion of (i).

To count, index the left cosets by themselves: consider the family $(C)_{C\in G/H}$ (Indexed Families of Sets and Their Union, Intersection and Product (i)), whose index set $G/H$ is finite. Its distinct members are disjoint by Left Cosets Partition a Group and All Have the Same Cardinality (i). The subgroup $H$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv), so each member $C=gH$ is finite with $\#C=\#H$ by Left Cosets Partition a Group and All Have the Same Cardinality (iii). The union of the family (Indexed Families of Sets and Their Union, Intersection and Product (ii)) is $G$: every $g\in G$ lies in $gH$ by Left Cosets Partition a Group and All Have the Same Cardinality (i), and every coset is a subset of $G$. Therefore The Number of Elements of a Disjoint Finite Union (ii) gives

$$\#G=\#(G/H)\cdot\#H,\qquad\text{that is,}\qquad |G|=[G:H]\cdot|H|,$$

by The Order of a Finite Group (i) and Cosets and the Index of a Subgroup (iv). This completes (i).

Since $[G:H]\in\mathbb{N}_{0}\subseteq\mathbb{Z}$, this identity exhibits $|G|$ as the integer multiple $k|H|$ of $|H|$ with $k=[G:H]$, so $|H|$ divides $|G|$ by Divisibility of Integers (i). This is (ii).