V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Epi (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (Subobject.arrow (kernelSubobject f)) f
refine' ⟨by simp, _⟩
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ IsIso (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Epi (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
refine' @IsIso.epi_of_iso _ _ _ _ _ ?_
no goals
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ IsIso (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
exact ⟨⟨factorThruImageSubobject _, by aesop_cat, by aesop_cat⟩⟩
no goals
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Subobject.arrow (kernelSubobject f) ≫ f = 0
simp
no goals
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) ≫
      factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) =
    𝟙 (Subobject.underlying.obj (imageSubobject (Subobject.arrow (kernelSubobject f))))
aesop_cat
no goals
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) ≫
      imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) =
    𝟙 (Subobject.underlying.obj (kernelSubobject f))
aesop_cat