Problem (2019CGMOp7): Let $DFGE$ be a cyclic quadrilateral. Line $DF$ intersects $EG$ at $C,$ and line $FE$ intersects $DG$ at $H.$ $J$ is the midpoint of $FG.$ The line $\ell$ is the reflection of the line $DE$ in $CH,$ and it intersects line $GF$ at $I.$ Prove that $C,J,H,I$ are concyclic.
AlphaGeometry formalization: b c e = triangle; f = on_circum b c e; a = on_line b f, on_line e c; p = on_line b e, on_line c f; d = on_line a p, on_line b c; m = midpoint f e; b1 = reflect b a d; c1 = reflect c a d; k = on_line b1 c1, on_line e f ? cyclic a m p k
HAGeo formalization: B C E = triangle; (BCE) = circle B C E; F = on_circle (BCE); BF = line B F; CE = line C E; A = intersection BF CE; BE = line B E; CF = line C F; P = intersection BE CF; AP = line A P; BC = line B C; D = intersection AP BC; M = midpoint E F; AD = line A D; B1 = reflect_point_wrt_line B AD; C1 = reflect_point_wrt_line C AD; B1C1 = line B1 C1; EF = line E F; K = intersection B1C1 EF; Prove: concyclic A M P K
Difficulty score: 3.7