case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → imageSubobject f = kernelSubobject g

case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ imageSubobject f = kernelSubobject g → Exact f g
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ imageSubobject f = kernelSubobject g
constructor
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ imageSubobject f = kernelSubobject g
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → imageSubobject f = kernelSubobject g
intro h
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageSubobject f = kernelSubobject g
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ imageSubobject f = kernelSubobject g
have : IsIso (imageToKernel f g h.w) := have := h.epi; isIso_of_mono_of_epi _
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ (asIso (imageToKernel f g (_ : f ≫ g = 0))).hom ≫ Subobject.arrow (kernelSubobject g) =
    Subobject.arrow (imageSubobject f)
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageSubobject f = kernelSubobject g
refine Subobject.eq_of_comm (asIso (imageToKernel _ _ h.w)) ?_
no goals
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ (asIso (imageToKernel f g (_ : f ≫ g = 0))).hom ≫ Subobject.arrow (kernelSubobject g) =
    Subobject.arrow (imageSubobject f)
simp
no goals
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ imageSubobject f = kernelSubobject g → Exact f g
apply exact_of_image_eq_kernel