Problem (2022SilkRoadp1): Convex quadrilateral $ABCD$ is inscribed in circle $w.$Rays $AB$ and $DC$ intersect at $K.\ L$ is chosen on the diagonal $BD$ so that $\angle BAC= \angle DAL.\ M$ is chosen on the segment $KL$ so that $CM \mid\mid BD.$ Prove that line $BM$ touches $w.$
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; k = on_line a b, on_line c d; l = on_line b d, on_aline l a d b a c; m = on_line k l, on_pline c b d; o = circumcenter a b c ? perp o b b m
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (ABC) = circle A B C; D = on_circle (ABC); AB = line A B; CD = line C D; K = intersection AB CD; BD = line B D; l1 = angle_equal1 A D B A C; L = intersection BD l1; KL = line K L; l2 = parallel_line C BD; M = intersection KL l2; OB = line O B; BM = line B M; Prove: perpendicular BM OB
Difficulty score: 2.5