Problem (2015USATSTp1): Let $ABC$ be a non-isosceles triangle with incenter $I$ whose incircle is tangent to $\overline{BC}$, $\overline{CA}$, $\overline{AB}$ at $D$, $E$, $F$, respectively. Denote by $M$ the midpoint of $\overline{BC}$. Let $Q$ be a point on the incircle such that $\angle AQD = 90^{\circ}$. Let $P$ be the point inside the triangle on line $AI$ for which $MD = MP$. Prove that either $\angle PQE = 90^{\circ}$ or $\angle PQF = 90^{\circ}$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i c a; f = foot i a b; m = midpoint b c; o1 = midpoint a d; q = on_circle i d, on_circle o1 a; p = on_line a i, on_circle m d ? perp p q q e
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; CA = line C A; AB = line A B; D = foot I BC; E = foot I CA; F = foot I AB; (I) = circle_center_point I D; M = midpoint B C; O1 = midpoint A D; (O1) = circle_center_point O1 A; Q = intersection (I) (O1); (M,D) = circle_center_point M D; AI = line A I; P = intersection AI (M,D); PQ = line P Q; QF = line Q F; Prove: perpendicular PQ QF
Difficulty score: 2.9