Problem (2016G4): Let $ABC$ be a triangle with $AB = AC \neq BC$ and let $I$ be its incentre. The line $BI$ meets $AC$ at $D$, and the line through $D$ perpendicular to $AC$ meets $AI$ at $E$. Prove that the reflection of $I$ in $AC$ lies on the circumcircle of triangle $BDE$.
AlphaGeometry formalization: a b c = iso_triangle; i = incenter a b c; d = on_line a c, on_line b i; e = on_line a i, on_tline d a c; i1 = reflect i a c ? cyclic b d e i1
HAGeo formalization: A B C = isos_triangle; I = incenter A B C; BI = line B I; AC = line A C; D = intersection BI AC; l1 = perpendicular_line D AC; AI = line A I; E = intersection l1 AI; I1 = reflect_point_wrt_line I AC; Prove: concyclic B D E I1
Difficulty score: 2.6