Problem (2010CHNWesternMOp2): $AB$ is a diameter of a circle with center $O$. Let $C$ and $D$ be two different points on the circle on the same side of $AB$, and the lines tangent to the circle at points $C$ and $D$ meet at $E$. Segments $AD$ and $BC$ meet at $F$. Lines $EF$ and $AB$ meet at $M$. Prove that $E,C,M$ and $D$ are concyclic.
AlphaGeometry formalization: a b = segment; o = midpoint a b; c = on_circle o a; d = on_circle o a; e = on_tline c o c, on_tline d o d; f = on_line a d, on_line b c; m = on_line e f, on_line a b ? cyclic e c m d
HAGeo formalization: A = point; B = point; O = midpoint A B; (O) = circle_center_point O A; C = on_circle (O); D = on_circle (O); l1 = tangent_line C (O); l2 = tangent_line D (O); E = intersection l1 l2; AD = line A D; BC = line B C; F = intersection AD BC; EF = line E F; AB = line A B; M = intersection EF AB; Prove: concyclic E C M D
Difficulty score: 2.1