∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M) (HN : N ≤ φ.ker), (QuotientAddGroup.lift N φ HN).ker = AddSubgroup.map (QuotientAddGroup.mk' N) φ.ker