Problem (2023KoMaLA840): The incircle of triangle $ABC$ touches the sides in $X$, $Y$ and $Z$. In triangle $XYZ$ the feet of the altitude from $X$ and $Y$ are $X'$ and $Y'$, respectively. Let line $X'Y'$ intersect the circumcircle of triangle $ABC$ at $P$ and $Q$. Prove that points $X$, $Y$, $P$ and $Q$ are concyclic.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; x = foot i b c; y = foot i a c; z = foot i a b; x1 = foot x y z; y1 = foot y x z; p = on_line x1 y1, on_circum a b c; q = on_line x1 y1, on_circum a b c ? cyclic x y p q
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; X = foot I BC; AC = line A C; Y = foot I AC; AB = line A B; Z = foot I AB; YZ = line Y Z; X1 = foot X YZ; XZ = line X Z; Y1 = foot Y XZ; X1Y1 = line X1 Y1; (ABC) = circle A B C; P = intersection X1Y1 (ABC); Q = intersection X1Y1 (ABC); Prove: concyclic X Y P Q
Difficulty score: 3.1