∀ (A : Type u_2) (E : Type u_6) [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E],
  ContinuousAddMonoidHom.instAddCommGroup A E =
    { toAddMonoid := inferInstance.toAddMonoid, neg := fun f => (ContinuousAddMonoidHom.neg E).comp f,
      sub := fun f g => { toAddMonoidHom := subAddMonoidHom, continuous_toFun := ⋯ }.comp (f.prod g),
      sub_eq_add_neg := ⋯, zsmul := zsmulRec, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
      add_comm := ⋯ }