Some basic lemmas for manipulating Ext over ModuleCat

theorem CategoryTheory.Abelian.Ext.postcomp_smul_id_eq_zero_of_mem_annihilator {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} {r : R} (mem_ann : r ∈ Module.annihilator R ↑N) (n : ℕ) : AddCommGrpCat.ofHom ((mk₀ (r • CategoryStruct.id M)).postcomp N ⋯) = 0

theorem CategoryTheory.Abelian.Ext.postcomp_smul_id_mono_iff {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} (r : R) (i : ℕ) : Mono (AddCommGrpCat.ofHom ((mk₀ (r • CategoryStruct.id M)).postcomp N ⋯)) ↔ IsSMulRegular (Ext N M i) r