∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal] [inst_2 : H.FiniteIndex],
  FiniteIndexNormalAddSubgroup.ofAddSubgroup H = { toAddSubgroup := H, isNormal' := ⋯, isFiniteIndex' := ⋯ }