Problem (2020G3): Let $ABCD$ be a convex quadrilateral with $\angle ABC>90$, $CDA>90$ and $\angle DAB=\angle BCD$. Denote by $E$ and $F$ the reflections of $A$ in lines $BC$ and $CD$, respectively. Suppose that the segments $AE$ and $AF$ meet the line $BD$ at $K$ and $L$, respectively. Prove that the circumcircles of triangles $BEK$ and $DFL$ are tangent to each other.
AlphaGeometry formalization: a b d = triangle; c = eqangle3 c b d a d b; e = reflect a b c; f = reflect a c d; k = on_line a e, on_line b d; l = on_line a f, on_line b d; o1 = circumcenter b e k; o2 = circumcenter d f l; t = on_circle o1 b, on_circle o2 d ? coll o1 o2 t
HAGeo formalization: A B D = triangle; ω1 = angle_equal2 B D D A B; C = on_circle ω1; BC = line B C; E = reflect_point_wrt_line A BC; CD = line C D; F = reflect_point_wrt_line A CD; AE = line A E; BD = line B D; K = intersection AE BD; AF = line A F; L = intersection AF BD; O1 = circumcenter B E K; O2 = circumcenter D F L; (O1) = circle_center_point O1 B; (O2) = circle_center_point O2 D; T = intersection (O1) (O2); Prove: collinear O1 O2 T
Difficulty score: 2.4