theorem QuotientGroups.quotient_group_composition {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] : Function.Surjective ⇑(QuotientGroup.mk' N) ∧ (QuotientGroup.mk' N).ker = N