Problem (2010G1): Let $ABC$ be an acute triangle with $D, E, F$ the feet of the altitudes lying on $BC, CA, AB$ respectively. One of the intersection points of the line $EF$ and the circumcircle is $P.$ The lines $BP$ and $DF$ meet at point $Q.$ Prove that $AP = AQ.$
AlphaGeometry formalization: a b c = triangle; d = foot a b c; e = foot b a c; f = foot c a b; o = circumcenter a b c; p = on_line e f, on_circle o a; q = on_line b p, on_line d f ? cong a p a q
HAGeo formalization: A B C = acute_triangle; BC = line B C; D = foot A BC; AC = line A C; E = foot B AC; AB = line A B; F = foot C AB; EF = line E F; O = circumcenter A B C; (O) = circle_center_point O A; P = intersection EF (O); BP = line B P; DF = line D F; Q = intersection BP DF; Prove: cong A P A Q
Difficulty score: 1.6