{G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        (G' : AddSubgroup G) →
          (H' : AddSubgroup H) →
            [inst_2 : G'.Normal] → [inst_3 : H'.Normal] → (e : G ≃+ H) → AddSubgroup.map (↑e) G' = H' → G ⧸ G' ≃+ H ⧸ H'