def SimpleGraph.IsMinor {W : Type u_1} {V : Type u_2} (H : SimpleGraph W) (G : SimpleGraph V) : Prop

H.IsMinor G asserts that H is a minor of G: there is a family of pairwise disjoint, nonempty, connected vertex subsets (branch sets) $\{f(w)\}_{w \in W}$ of G such that whenever $w_1$ and $w_2$ are adjacent in H, there is an edge in G between the branch sets $f(w_1)$ and $f(w_2)$.

theorem SimpleGraph.hadwiger_conjecture (t : ℕ) (ht : t ≥ 1) (V : Type u_3) (G : SimpleGraph V) (hG : ¬(completeGraph (Fin (t + 1))).IsMinor G) : G.Colorable t

Hadwiger's conjecture (Conjecture 5.3.1, Hadwiger 1936). For every $t \geq 1$, any graph $G$ that does not contain $K_{t+1}$ as a minor is $t$-colorable.