This post is devoted to the rigorous proof of Miquel's five circles theorem, which I learned about from this question. The proof is essentially very simple and takes only 15 lines of code. The figure below, in which all the labels coincide with the corresponding names in the code, illustrates the basic ideas of the code. First, we symbolically define common points of intersection of blue circles with a red unit circle (these parameters s1 .. s5 are the polar coordinates of these points). All other parameters of this configuration can be expressed through them. Then we find the centers M and N of two circles. Then we find the coordinates of the point K from the condition that CK is perpendicular to MN . Then we find the point E and using the result obtained, we easily find the coordinates of all the points A1 .. A5. Then we find the coordinates of the point P as the point of intersection of the lines A1A2 and A3A4 . Finally, we verify that the point P lies on a circle with center at the point N , which completes the proof.
Below - the code of the proof. Note that the code does not use any special (in particular geometric) packages, only commands from the Maple kernel. I usually try any geometric problems to solve in this style, it is more reliable, and often shorter.
is(eval(Circle, P)=0); # The final result
It may seem that this proof is easy to repeat manually. But this is not so. Maple brilliantly coped with very cumbersome trigonometric transformations. Look at the coordinates of point P , expressed through the initial parameters s1 .. s5 :
simplify(eval([x,y], P)); # The coordinates of the point P