∀ {G : Type u} [inst : AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal]
  [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B),
  QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h =
    QuotientAddGroup.map (A'.addSubgroupOf A) (B'.addSubgroupOf B) (AddSubgroup.inclusion h) ⋯