CMO2023 Product of segements

[Landau1994]

According to study the grammer of the input of alphageometry, I can tranlated the power of point theorem as follows

a b c = triangle a b c; d = circle d a b c; e = on_circle e d a; f = intersection_ll f a e c b ? eqratio f e f b f c f a

And the output of alphageometry is

==========================
 * From theorem premises:
A B C D E F : Points
DA = DB [00]
DB = DC [01]
DE = DA [02]
E,A,F are collinear [03]
C,B,F are collinear [04]

 * Auxiliary Constructions:
: Points

 * Proof steps:
001. DA = DB [00] & DE = DA [02] & DB = DC [01] ⇒  C,E,B,A are concyclic [05]
002. C,E,B,A are concyclic [05] ⇒  ∠CBE = ∠CAE [06]
003. E,A,F are collinear [03] & C,B,F are collinear [04] & ∠CAE = ∠CBE [06] ⇒  ∠CAF = ∠FBE [07]
004. C,B,F are collinear [04] & E,A,F are collinear [03] ⇒  ∠CFA = ∠BFE [08]
005. ∠CAF = ∠FBE [07] & ∠CFA = ∠BFE [08] (Similar Triangles)⇒  CF:AF = EF:BF
==========================

This is very easy.

But when I try to formalize a more complicated problem of CMO 2023, i realized it seems very hard to fromalized the conculusion involved three segements products. Can anyone else have a good idea? ( I translated the questions as follows)

In an acute-angled triangle ABC, B, C, K are collinear but K is outside the segments of BC, KP // AB, KQ // KC。 If BK=BP, CK=CQ, and cirmucircle of triangle intersect AK in T: Please Proof: 1) $\angle BTC + \angle APB = \angle CQA$; 2) $AP\cdot BT \cdot CQ = AQ \cdot CT \cdot BP$

[Landau1994]

According to suggestions in this https://www.zhihu.com/question/640049082 , like the alphafold author, we can translate the cmo problem to this form Because by the power of point, $$\begin{align} & AD\cdot AP = AE \cdot AQ, AD=CQ \ & \Leftrightarrow \frac{AP\cdot CQ}{AQ} = AE \ & BG\cdot BT = BP \cdot BF, BF = CT \ & \Leftrightarrow \frac{BP \cdot CT}{BT} = BG \ & AP \cdot BT \cdot CQ = AQ \cdot CT \cdot BP \ & \Leftrightarrow AE = BG \end{align} $$ And alphageometry can solve the second part by prove $AE=BG$ now! This is the input

reduced_cmo_2023_p5
a b c = triangle a b c; k = on_line k b c; p = on_pline p k a b, on_circle p b k; q = on_pline q k a c, on_circle q c k; y = circle p k q; t = on_circle t y k, on_line t a k; z1 = on_line z1 p q; d = on_line d a p, eqdistance d a q c; f = on_line f p b, eqdistance f b c t; y1 = circle p d q; y2 = circle p f t; e = on_circle e y1 q, on_line q a; g = on_circle g y2 t, on_line g t b ? cong a e b g

This is the output proof!

==========================
 * From theorem premises:
A B C D E F G H J K L M N O : Points
C,D,B are collinear [00]
BE = BD [01]
ED ∥ AB [02]
CF = CD [03]
FD ∥ AC [04]
GD = GF [05]
GE = GD [06]
H,D,A are collinear [07]
GH = GD [08]
JA = FC [09]
J,E,A are collinear [10]
KB = CH [11]
K,E,B are collinear [12]
LJ = LF [13]
LE = LJ [14]
MK = MH [15]
ME = MK [16]
F,N,A are collinear [17]
LN = LF [18]
O,H,B are collinear [19]
MO = MH [20]

 * Auxiliary Constructions:
Q : Points
QH = QD [21]
H,Q,D are collinear [22]

 * Proof steps:
001. LJ = LF [13] & LN = LF [18] & LE = LJ [14] ⇒  F,J,N,E are concyclic [23]
002. F,J,N,E are concyclic [23] ⇒  ∠FNJ = ∠FEJ [24]
003. F,A,N are collinear [17] & ∠FNJ = ∠FEJ [24] & J,E,A are collinear [10] ⇒  ∠FEA = ∠ANJ [25]
004. F,N,A are collinear [17] & J,E,A are collinear [10] ⇒  ∠FAE = ∠NAJ [26]
005. ∠FEA = ∠ANJ [25] & ∠FAE = ∠NAJ [26] (Similar Triangles)⇒  FE:FA = JN:JA [27]
006. ∠FEA = ∠ANJ [25] & ∠FAE = ∠NAJ [26] (Similar Triangles)⇒  FE:EA = JN:NA [28]
007. MK = MH [15] & MO = MH [20] & ME = MK [16] ⇒  K,H,O,E are concyclic [29]
008. K,H,O,E are concyclic [29] ⇒  ∠KOH = ∠KEH [30]
009. H,O,B are collinear [19] & ∠KOH = ∠KEH [30] & K,E,B are collinear [12] ⇒  ∠BEH = ∠KOB [31]
010. K,E,B are collinear [12] & ∠KOH = ∠KEH [30] & O,H,B are collinear [19] ⇒  ∠BHE = ∠OKB [32]
011. ∠BEH = ∠KOB [31] & ∠BHE = ∠OKB [32] (Similar Triangles)⇒  BE:BH = BO:BK [33]
012. BE:BH = BO:BK [33] & BE = BD [01] & KB = CH [11] ⇒  DB:HB = OB:CH [34]
013. CF = CD [03] & GD = GF [05] ⇒  DF ⟂ CG [35]
014. BE = BD [01] & GE = GD [06] ⇒  DE ⟂ BG [36]
015. DF ⟂ CG [35] & DF ∥ AC [04] & DE ⟂ BG [36] & DE ∥ AB [02] ⇒  ∠GBA = ∠GCA [37]
016. ∠GBA = ∠GCA [37] ⇒  C,B,G,A are concyclic [38]
017. GH = GD [08] & QH = QD [21] ⇒  HD ⟂ GQ [39]
018. H,Q,D are collinear [22] & H,D,A are collinear [07] & HD ⟂ GQ [39] & DE ⟂ BG [36] & DE ∥ AB [02] ⇒  ∠GBA = ∠GQA [40]
019. ∠GBA = ∠GQA [40] ⇒  Q,B,G,A are concyclic [41]
020. C,B,G,A are concyclic [38] & Q,B,G,A are concyclic [41] ⇒  Q,C,B,A are concyclic [42]
021. Q,C,B,A are concyclic [42] ⇒  ∠CQA = ∠CBA [43]
022. Q,C,B,A are concyclic [42] ⇒  ∠CAQ = ∠CBQ [44]
023. H,Q,D are collinear [22] & H,D,A are collinear [07] & C,D,B are collinear [00] & ∠CQA = ∠CBA [43] ⇒  ∠CQD = ∠DBA [45]
024. C,D,B are collinear [00] & H,Q,D are collinear [22] & H,D,A are collinear [07] ⇒  ∠CDQ = ∠BDA [46]
025. ∠CQD = ∠DBA [45] & ∠CDQ = ∠BDA [46] (Similar Triangles)⇒  CQ:QD = BA:DB [47]
026. CQ:QD = BA:DB [47] & QH = QD [21] & EB = DB [01] ⇒  QC:QH = BA:BE [48]
027. BE = BD [01] ⇒  ∠BDE = ∠DEB [49]
028. C,D,B are collinear [00] & K,B,E are collinear [12] & ∠BDE = ∠DEB [49] ⇒  ∠EDC = ∠KED [50]
029. C,D,B are collinear [00] & H,Q,D are collinear [22] & H,D,A are collinear [07] & ∠CQA = ∠CBA [43] & AB ∥ DE [02] ⇒  ∠DCQ = ∠(DE-QH) [51]
030. ∠EDC = ∠KED [50] & ∠DCQ = ∠(DE-QH) [51] ⇒  ∠(DE-CQ) = ∠(KE-QH) [52]
031. H,Q,D are collinear [22] & H,D,A are collinear [07] & ∠(DE-CQ) = ∠(KE-QH) [52] & K,E,B are collinear [12] & DE ∥ AB [02] ⇒  ∠CQH = ∠ABE [53]
032. QC:QH = BA:BE [48] & ∠CQH = ∠ABE [53] (Similar Triangles)⇒  CQ:CH = BA:EA [54]
033. C,D,B are collinear [00] & H,Q,D are collinear [22] & H,D,A are collinear [07] & ∠CAQ = ∠CBQ [44] ⇒  ∠DCA = ∠BQD [55]
034. C,D,B are collinear [00] & ∠CAQ = ∠CBQ [44] & H,Q,D are collinear [22] & H,D,A are collinear [07] ⇒  ∠DAC = ∠QBD [56]
035. ∠DCA = ∠BQD [55] & ∠DAC = ∠QBD [56] (Similar Triangles)⇒  CD:CA = QD:QB [57]
036. CD:CA = QD:QB [57] & JA = FC [09] & CF = CD [03] & QH = QD [21] ⇒  CF:CA = QH:QB [58]
037. CF = CD [03] ⇒  ∠CDF = ∠DFC [59]
038. C,D,B are collinear [00] & H,Q,D are collinear [22] & H,D,A are collinear [07] & ∠CAQ = ∠CBQ [44] & AC ∥ DF [04] ⇒  ∠(CD-QB) = ∠(DF-QH) [60]
039. ∠CDF = ∠DFC [59] & ∠(CD-QB) = ∠(DF-QH) [60] ⇒  ∠(CF-QH) = ∠(DF-QB) [61]
040. H,Q,D are collinear [22] & H,D,A are collinear [07] & ∠(CF-QH) = ∠(DF-QB) [61] & DF ∥ AC [04] ⇒  ∠FCA = ∠HQB [62]
041. CF:CA = QH:QB [58] & ∠FCA = ∠HQB [62] (Similar Triangles)⇒  FC:FA = HQ:HB [63]
042. FC:FA = HQ:HB [63] & JA = FC [09] & QH = QD [21] ⇒  JA:FA = QD:HB [64]
043. BE = BD [01] & JA = FC [09] & KB = CH [11] & QH = QD [21] & FE:FA = JN:JA [27] & FE:EA = JN:NA [28] & DB:HB = OB:CH [34] & CQ:QD = BA:DB [47] & CQ:CH = BA:EA [54] & JA:FA = QD:HB [64] (Ratio chase)⇒  NA = OB
==========================