cancelling an isomorphism in a concrete abelian category

Stream: Is there code for X?

[Kevin Buzzard]

Hello! Abelian category learner here. Do we have things like this:

import algebra.category.Group

lemma iso_equiv_inv_apply_eq_zero_cancel
  {A B C : AddCommGroup} {a : A} {f : A ⟶ B} {e : C ≅ B}
  (h : (f ≫ e.inv) a = 0) : f a = 0 :=
begin
  rw category_theory.comp_apply at h,
  apply_fun e.hom at h,
  rwa [category_theory.coe_inv_hom_id, map_zero] at h,
end

? And if so, what's its name?