case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ Exact f g → f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0

case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → Exact f g
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ Exact f g ↔ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
constructor
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : Exact f g
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ Exact f g → f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
intro h
no goals
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : Exact f g
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
exact ⟨h.1, fork_ι_comp_cofork_π f g h cg cf⟩
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → Exact f g
rw [exact_iff]
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
⊢ f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0 → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
refine fun h => ⟨h.1, ?_⟩
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ (IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f = 0
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
apply zero_of_epi_comp (IsLimit.conePointUniqueUpToIso hg (limit.isLimit _)).hom
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ ((IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f) ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)) hf).hom =
    0
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ (IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f = 0
apply zero_of_comp_mono (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) hf).hom
no goals
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
cg : KernelFork g
hg : IsLimit cg
cf : CokernelCofork f
hf : IsColimit cf
h : f ≫ g = 0 ∧ Fork.ι cg ≫ Cofork.π cf = 0
⊢ ((IsLimit.conePointUniqueUpToIso hg (limit.isLimit (parallelPair g 0))).hom ≫ kernel.ι g ≫ cokernel.π f) ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)) hf).hom =
    0
simp [h.2]