Problem (2019GOTEEMp2): Let $ABC$ be an acute triangle with $AB \neq AC$, and let $D, E, F$ be the feet of the altitudes from $A, B, C$, respectively. Let $P$ be a point on $DE$ such that $AP \perp AB$ and let $Q$ be a point on $DF$ such that $AQ \perp AC$. Lines $PQ$ and $BC$ intersect at $T$. If $M$ is the midpoint of $\overline{BC}$, prove that $\angle MAT = 90^\circ$.
AlphaGeometry formalization: a b c = triangle; d = foot a b c; e = foot b a c; f = foot c a b; p = on_line d e, on_tline a a b; q = on_line d f, on_tline a a c; t = on_line p q, on_line b c; m = midpoint b c ? perp m a a t
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; l1 = perpendicular_line A AB; DE = line D E; P = intersection DE l1; l2 = perpendicular_line A AC; DF = line D F; Q = intersection DF l2; PQ = line P Q; T = intersection PQ BC; M = midpoint B C; AM = line A M; AT = line A T; Prove: perpendicular AM AT
Difficulty score: 2.7