C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
ex : Exact f g
this : IsIso (kernel.lift g f (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (kernel.lift g f (_ : f ≫ g = 0)));
  CategoryTheory.inv (kernel.lift g f (_ : f ≫ g = 0)) ≫ f = kernel.ι g
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
ex : Exact f g
⊢ let_fun this := (_ : IsIso (kernel.lift g f (_ : f ≫ g = 0)));
  CategoryTheory.inv (kernel.lift g f (_ : f ≫ g = 0)) ≫ f = kernel.ι g
have := isIso_kernel_lift_of_exact_of_mono _ _ ex
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono f
ex : Exact f g
this : IsIso (kernel.lift g f (_ : f ≫ g = 0))
⊢ let_fun this := (_ : IsIso (kernel.lift g f (_ : f ≫ g = 0)));
  CategoryTheory.inv (kernel.lift g f (_ : f ≫ g = 0)) ≫ f = kernel.ι g
simp