$|L(1,\chi)| \le 6\log q$ for non-principal $\chi$

The bound $L(1,\chi) \ll \log q$. Let $q \ge 1$ and let $\chi$ be a non-principal Dirichlet character modulo $q$. Then

This is the classical estimate $L(1,\chi) \ll \log q$ (the case $s = 1$ of Montgomery–Vaughan, Lemma 10.15), with an explicit admissible constant. It follows from the partial-summation representation $L(1,\chi) = \int_1^\infty S(x)\,x^{-2}\,dx$ with $S(x) = \sum_{n\le x}\chi(n)$, using $|S(x)| \le x$ for $x \le q$ and $|S(x)| \le q$ for $x \ge q$, which gives $|L(1,\chi)| \le \log q + 1$; the constant $6$ leaves room for the constants of the Lean argument. In Siegel's theorem it converts a lower bound for $L(1,\chi_1)L(1,\chi_2)L(1,\chi_1\chi_2)$ into a lower bound for $L(1,\chi_2)$ at the cost of a factor $\log(q_1q_2)$.

Formalization Note. A non-principal character exists only for $q \ge 3$, where $\log q > 1$, so the right-hand side is positive whenever the statement is not vacuous.