∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }