Kervaire–Milnor: $|\pi_0\,\mathrm{Diff}(S^6)| = 56$

Let $\mathrm{Diff}(S^6)$ be the group of all smooth diffeomorphisms of the round unit sphere $S^6\subset\mathbb R^7$ with the $C^\infty$ topology. Then its set of path components (isotopy classes of diffeomorphisms) has exactly $56$ elements:

This is one of the groups $\pi_0\mathrm{Diff}(S^n)$, $n\ge5$, that the source says were computed by relating them to Kervaire–Milnor's groups of homotopy spheres: $\pi_0\mathrm{Diff}^+(S^6)\cong\Theta_7\cong\mathbb Z/28$ (Cerf's pseudo-isotopy theorem together with Smale's $h$-cobordism theorem and Kervaire–Milnor), and orientation-reversing diffeomorphisms double the count. It is a concrete higher-dimensional instance of the kind of computation that is open for $n=4$.

Formalization Note ZerothHomotopy X is the set of path components of $X$; Nat.card is its cardinality (it would be $0$ if the set were infinite, so the statement also asserts finiteness).