Problem (2008AsiaPacificMOp3): Let $ \Gamma$ be the circumcircle of a triangle $ ABC$. A circle passing through points $ A$ and $ C$ meets the sides $ BC$ and $ BA$ at $ D$ and $ E$, respectively. The lines $ AD$ and $ CE$ meet $ \Gamma$ again at $ G$ and $ H$, respectively. The tangent lines of $ \Gamma$ at $ A$ and $ C$ meet the line $ DE$ at $ L$ and $ M$, respectively. Prove that the lines $ LH$ and $ MG$ meet at $ \Gamma$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; o1 = on_bline a c; d = on_line b c, on_circle o1 a; e = on_line b a, on_circle o1 a; g = on_line a d, on_circum a b c; h = on_line c e, on_circum a b c; l = on_line d e, on_tline a o a; m = on_line d e, on_tline c o c; x = on_line l h, on_line m g ? cyclic a b c x
HAGeo formalization: A B C = triangle; O = circumcenter A B C; l1 = perpendicular_bisector A C; O1 = on_line l1; (O1) = circle_center_point O1 A; BC = line B C; D = intersection (O1) BC; AB = line A B; E = intersection (O1) AB; AD = line A D; (ABC) = circle A B C; G = intersection AD (ABC); CE = line C E; H = intersection CE (ABC); OA = line O A; t1 = perpendicular_line A OA; DE = line D E; L = intersection t1 DE; OC = line O C; t2 = perpendicular_line C OC; M = intersection t2 DE; HL = line H L; GM = line G M; X = intersection HL GM; Prove: concyclic A B C X
Difficulty score: 2.7