∀ {G : Type u_2} {H : Type u_1} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : H ⧸ H'),
  (QuotientGroup.map G' H' ↑e ⋯) ((QuotientGroup.map H' G' ↑e.symm ⋯) x) = x