What route to take to Chebotarev?

Stream: PrimeNumberTheorem+

[Terence Tao]

I am not myself an expert in algebraic number theory, but my colleague Romyar Sharifi kindly pointed me towards his lecture notes where he proves (the Dirichlet density version of) the Chebotarev density theorem in Section 7. Roughly speaking, the idea is to first prove Chebotarev for cyclotomic extensions, then for abelian extensions (which in particular covers the case of cyclic extensions), and then arbitrary extensions. The latter two steps are mostly algebraic number theory in nature; it is just the first step in which analytic methods are used. It seems the cyclotomic case is very similar in spirit to the prime number theorem in arithmetic progressions (and indeed generalizes that theorem). I made a preliminary attempt to state some of the key steps in the blueprint at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/222 , focusing on the cyclotomic case. But I am not very confident that this is the optimal route, I'm hoping there is someone who is more familiar with the algebraic number theory side of things who can chime in.