"The first formal proof of the Jordan curve theorem was created by Hales in the HOL Light system, in January 2005, and contained about 60,000 lines. Another rigorous 6,500-line formal proof was produced in 2005 by an international team of mathematicians using the Mizar system. Both the Mizar and the HOL Light proof rely on libraries of previously proved theorems, so these two sizes are not comparable."
But for an even more obvious theorem that was actually difficult to prove (Rolle's theorem isn't), see https://en.wikipedia.org/wiki/Jordan_curve_theorem
("Any path which begins in the interior of a closed curve, and ends in the exterior of the same curve, must cross the curve at some point.")