Problem (2017ARMOg10p2): Let $ABC$ be an acute angled isosceles triangle with $AB=AC$ and circumcentre $O$. Lines $BO$ and $CO$ intersect $AC, AB$ respectively at $B', C'$. A straight line $l$ is drawn through $C'$ parallel to $AC$. Prove that the line $l$ is tangent to the circumcircle of $\triangle B'OC$.
AlphaGeometry formalization: a b c = iso_triangle; o = circumcenter a b c; b1 = on_line a c, on_line b o; c1 = on_line a b, on_line c o; o2 = circumcenter b1 o c; s = parallelogram a c c1 s; f = foot o2 c1 s ? cong o2 f o2 b1
HAGeo formalization: A B C = isos_triangle; O = circumcenter A B C; BO = line B O; AC = line A C; B1 = intersection BO AC; CO = line C O; AB = line A B; C1 = intersection CO AB; l = parallel_line C1 AC; O2 = circumcenter B1 O C; F = foot O2 l; Prove: cong O2 F O2 B1
Difficulty score: 1.7