C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
ex : Exact f g
this : IsIso (cokernel.desc f g (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (cokernel.desc f g (_ : f ≫ g = 0)));
  g ≫ CategoryTheory.inv (cokernel.desc f g (_ : f ≫ g = 0)) = cokernel.π f
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
ex : Exact f g
⊢ let_fun this := (_ : IsIso (cokernel.desc f g (_ : f ≫ g = 0)));
  g ≫ CategoryTheory.inv (cokernel.desc f g (_ : f ≫ g = 0)) = cokernel.π f
have := isIso_cokernel_desc_of_exact_of_epi _ _ ex
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi g
ex : Exact f g
this : IsIso (cokernel.desc f g (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (cokernel.desc f g (_ : f ≫ g = 0)));
  g ≫ CategoryTheory.inv (cokernel.desc f g (_ : f ≫ g = 0)) = cokernel.π f
simp