∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y],
  addEquivIsoAddSemigrpIso =
    { hom := fun e => e.toAddSemigrpIso, inv := fun i => i.addSemigrpIsoToAddEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }