∀ {G : Type u_5} [inst : AddCommGroup G] (N : AddSubgroup G),
  QuotientAddGroup.Quotient.addCommGroup N =
    {
      toAddGroup :=
        have this := ⋯;
        QuotientAddGroup.Quotient.addGroup N,
      add_comm := ⋯ }