The extremal function for K9= minors

We prove the extremal function for $K_9^{=}$ minors, where $K_9^{=}$ denotes the complete graph $K_9$ with two edges removed. In particular, we show that any graph with $n\ge 8$ vertices and at least $6n-20$ edges either contains a $K_9^{=}$ minor or is isomorphic to a graph obtained from disjoint copies of $K_8$ and $K_{2,2,2,2,2}$ by identifying cliques of size 5. We utilize computer assistance to prove one of our lemmas.