Quotient by a closed normal subgroup is a Lie group

Normality makes $(gN)(hN)=ghN$ and $(gN{)}^{-1}=g^{-1}N$ independent of representatives. These operations satisfy the group axioms because the operations on $G$ do, and $q$ is algebraically a surjective homomorphism. They are the only possible operations with this property, since every coset has a representative.

Normality also gives ${\mathrm{Ad}}_g(\mathfrak{n})=\mathfrak{n}$ for every $g$: conjugation by $g$ restricts to a diffeomorphism of $N$. For $X\in \mathfrak{g}$ and $Y\in \mathfrak{n}$, the curve $t\mapsto {\mathrm{Ad}}_{\exp (tX)}Y$ lies in $\mathfrak{n}$; its derivative at zero is $[X,Y]$ by [F2]. Thus $\mathfrak{n}$ is an ideal. Define $[X+\mathfrak{n},Y+\mathfrak{n}]=[X,Y]+\mathfrak{n}$; replacing either representative by an element of $\mathfrak{n}$ changes the bracket by an element of $\mathfrak{n}$. Bilinearity, antisymmetry, and Jacobi descend, so this is a Lie bracket on $\mathfrak{g}\mathrm{/}\mathfrak{n}$.

The descended inversion is smooth: on a quotient-chart neighborhood choose a smooth local section $s$ of $q$; there it is $x\mapsto q(s(x{)}^{-1})$. Similarly, near $(x,y)$ choose local sections $s_1,s_2$ and write multiplication as $(x^{\mathrm{\prime }},y^{\mathrm{\prime }})\mapsto q(s_1(x^{\mathrm{\prime }})s_2(y^{\mathrm{\prime }}))$. These formulas are smooth and agree on overlaps by representative independence. Hence $G\mathrm{/}N$ is a Lie group and $q$ is smooth.

By [F2], $d{q}_e:\mathfrak{g}\to \mathrm{Lie}(G\mathrm{/}N)$ is a Lie-algebra homomorphism. By [A1] it is surjective with kernel $\mathfrak{n}$, so its induced linear isomorphism $\mathfrak{g}\mathrm{/}\mathfrak{n}\to \mathrm{Lie}(G\mathrm{/}N)$ preserves brackets and is the claimed canonical Lie-algebra isomorphism.

Uniqueness of the smooth manifold structure is in [A1], and uniqueness of the operations is step 1.1. The cases $N=G$, $N=\{e\}$, and disconnected groups are included. Normality, not merely closedness, is used precisely in steps 1.1 and 1.2. Countable choice is inherited through [A1] and [F2].