Problem (2019RMMp2): Let $ABCD$ be an isosceles trapezoid with $AB\parallel CD$. Let $E$ be the midpoint of $AC$. Denote by $\omega$ and $\Omega$ the circumcircles of the triangles $ABE$ and $CDE$, respectively. Let $P$ be the crossing point of the tangent to $\omega$ at $A$ with the tangent to $\Omega$ at $D$. Prove that $PE$ is tangent to $\Omega$.
AlphaGeometry formalization: a b c d = eq_trapezoid; e = midpoint a c; o1 = circumcenter a b e; o2 = circumcenter c d e; p = on_tline a o1 a, on_tline d o2 d ? perp p e o2 e
HAGeo formalization: A D C B = isos_trapezoid; E = midpoint A C; O1 = circumcenter A B E; O2 = circumcenter C D E; O1A = line O1 A; O2D = line O2 D; l1 = perpendicular_line A O1A; l2 = perpendicular_line D O2D; P = intersection l1 l2; EP = line E P; O2E = line O2 E; Prove: perpendicular EP O2E
Difficulty score: 3.3