24th Korean Mathematical Olympiad Final Round

Let $T$ be the intersection point of $ED$ and the circumcircle of $ABC$ other than $E$. Since $\angle CTD=\angle EFD$ and $\angle CDT=\angle EDF$, $DCT$ and $DEF$ are similar triangles. Hence $$\frac{EF}{DF}=\frac{TC}{DT}$$ Note that $AE$ is the perpendicular bisector of the line segment $CD$, as $AD=AC$ and $\angle DAE=\angle CAE$. It follows that $EB=EC=ED$, which means that $E$ is the circumcenter of the triangle $BCD$. Thus $\angle BEF=\angle DEF$. This implies that $CD$ is the angle bisector of $\angle TCK$. In fact, since $\angle TCB=\angle TEB$, $\angle TCB=2\angle BEF$. Then $\angle TCB=2\angle BCD$ comes from $\angle BEF=\angle BCD$. In a triangle $CKT$, $CD$ being the angle bisector of $\angle TCK$ gives rise to the following: $$\frac{TC}{DT}=\frac{KC}{DK}$$

From this along with the result obtained above, we obtain $\frac{EF}{DF}=\frac{KC}{DK}$. Thus, $$DK\cdot EF=KC\cdot DF.$$ Now since $DK\cdot EF=KC\cdot DF$, $$DK\cdot EF=AC\cdot DF⟺AC\cdot DF=KC\cdot DF.$$ But, since $AB>AC$, $D\ne B$, and so $DF\ne 0$. Therefore $$DK\cdot EF=AC\cdot DF⟺CK=AC.$$