The lattice isomorphism/correspondence theorem for groups is an elegant statement about (normal) subgroups of $G$ containing $N$ corresponding with (normal) subgroups of $G/N$. However, I am not aware of any clean/streamlined proof (in Dummit & Foote and Aluffi, it is brushed over as an exercise). Does anyone have such a streamlined proof?
For reference, here is my "ugly" proof, which is very long and perhaps even wrong: $\newcommand{\quot}[2]{#1/#2} \newcommand{\normaleq}{\trianglelefteq}$ For a normal subgroup $N \normaleq G$, we prove that the map $\varphi$ defined by $H \mapsto \quot H N$ establishes
a bijection between subgroups of $G$ containing $N$ and subgroups of $\quot GN$.
Well-defined: we check that for a subgroup $H \leq G$ containing $N$, $\quot HN$ is actually a subgroup of $\quot GN$. Well, $e\in H \implies eN = e_{G/N} \in \quot HN$; associativity is inherited from $\quot GN$; $g,h\in H \implies (gN)(hN) =: (gh)N \in \quot HN$; and $g\in H \implies (gN)^{-1} = g^{-1} N \in \quot HN$.
Inverse: we construct an explicit inverse using the canonical projection $\pi : G \to \quot GN$ ($g\mapsto gN$), namely we show that $\pi^{-1}$ is the desired inverse. First, we want to show for a subgroup $H \leq G$ containing $N$, $\pi^{-1}(\quot HN) := \{g\in G: gN \in \quot HN\} = H$. The ($\supseteq$) containment is true because $h\in H \implies hN \in \quot HN$; and the ($\subseteq$) containment is true because $\quot HN = \{hN : h \in H\}$ implying that $gN \in \quot HN \implies gN = hN$ for some $h\in H$, i.e. $g = hn \in H$ since $n$ is some element of $N \subseteq H$.
Second, we show that for a subgroup $S$ of $\quot GN$, $\pi^{-1}(S)$ is a subgroup of $G$ containing $N$, and $\varphi(\pi^{-1}(S)) = S$. We know that inverse images via homomorphisms are subgroups, and since $S$ in particular contains $e_{G/N}$, the inverse image $\pi^{-1}(S) \supseteq \pi^{-1}(\{e_{G/N}\}) = \ker(\pi) = N$. Next suppose that $g\in \pi^{-1}(S) \implies \pi(g) = gN \in S$. This tells us that $\varphi(\pi^{-1}(S)) \subseteq S$. Now suppose $gN \in S$. (i.e. is an arbitary element of $S \leq \quot GN$ since its elements are all of the form $gN$ for some $g\in G$). Well, $\pi(g) = gN \in S \implies g\in \pi^{-1}(S) \implies gN \in \varphi(\pi^{-1}(S))$, and so $S \subseteq \varphi(\pi^{-1}(S))$, completing the proof.
a bijection between normal subgroups of $G$ containing $N$ and normal subgroups of $\quot GN$.
Well-defined: we check that for a normal subgroup $H \leq G$, $\quot HN$ is actually a normal subgroup of $\quot GN$. In part (a) above, we already verified all the "subgroup" related claims, so we just need to verify normality. Let $h\in H$ be arbitrary. Then for any $g\in G$, we have $(gN)(hN)(gN)^{-1} = ghg^{-1} N$, but since $ghg^{-1} \in H$, $ghg^{-1} N \in \quot H N$, so indeed $\quot HN$ is normal in $\quot GN$.
Inverse: we construct an explicit inverse using the canonical projection $\pi : G \to \quot GN$ ($g\mapsto gN$), namely we show that $\pi^{-1}$ is the desired inverse. In part (a) above, we already verified all the "subgroup" related claims, so we just need to verify normality, namely that the inverse image of a normal subgroup is normal. Well if $x\in \pi^{-1}(S)$ for a normal subgroup $S \normaleq GN$, then for any $g \in G$, $gxg^{-1}$ will satisfy $\pi(gxg^{-1}) = \pi(g) \pi(x) \pi(g^{-1}) \in S$ (since $\pi(x) \in S$ and $S$ is normal), so indeed $gxg^{-1} \in \pi^{-1}(S)$. But $x\in \pi^{-1}(S)$ was arbitrary, so $g \pi^{-1}(S) g^{-1} \subseteq \pi^{-1}(S)$ for all $g\in G$, which suffices to prove that $\pi^{-1}(S) \normaleq G$ (since $gNg^{-1} \subseteq N \implies Ng^{-1} \subseteq g^{-1} N$ and also $gN \subseteq Ng$ where again $g$ is taken over all of $G$).