no goals
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup α
inst✝ : AddCommGroup β
f g : α → β
hf : IsAddGroupHom f
hg : IsAddGroupHom g
⊢ IsAddGroupHom fun a => f a - g a
simpa only [sub_eq_add_neg] using hf.add hg.neg