Problem (2022CGMOp3): In triangle $ABC,AB>AC,I$ is the incenter, $AM$ is the midline. The line crosses $I$ and is perpendicular to $BC $ intersect $AM$ at point $L$, and the symmetry of $I$ with respect to point $A$ is $J$ Prove that: $\angle ABJ= \angle LBI$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; m = midpoint b c; l = on_tline i b c, on_line a m; j = mirror i a ? eqangle a b b j i b b l
HAGeo formalization: A B C = triangle; I = incenter A B C; M = midpoint B C; BC = line B C; l1 = perpendicular_line I BC; AM = line A M; L = intersection AM l1; J = reflect_point_wrt_point I A; Prove: equal_angle A B J I B L
Difficulty score: 3.5