∀ {G : Type u} [inst : AddGroup G] {M N : AddSubgroup G} [inst_1 : M.Normal] [inst_2 : N.Normal] (h : M = N),
  QuotientAddGroup.quotientAddEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, map_add' := ⋯ }