def CorrespondenceTheorem.correspondenceOrderIso {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) : { H : Subgroup G // f.ker ≤ H } ≃o Subgroup G'