∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [hn : N.Normal] (H : Subgroup G) (hH : N ≤ H),
  ↑((fun H' => ⟨Subgroup.comap (QuotientGroup.mk' N) H', ⋯⟩)
        ((fun H => Subgroup.map (QuotientGroup.mk' N) ↑H) ⟨H, hH⟩)) =
    ↑⟨H, hH⟩