-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_of_forks {cg : KernelFork S.g} (hg : IsLimit cg) {cf : CokernelCofork S.f}
    (hf : IsColimit cf) : S.Exact ↔ cg.ι ≫ cf.π = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ : ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g = Fork.ι cg
eq₂ : cokernel.π S.f ≫ ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom = Cofork.π cf
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
rw [← eq₁, ← eq₂, Category.assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
eq₂ :
  (Cofork.ofπ (cokernel.π S.f) ⋯).ι.app WalkingParallelPair.one ≫
      ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom =
    cf.ι.app WalkingParallelPair.one
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
dsimp at eq₁ eq₂

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ : ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g = Fork.ι cg
eq₂ : cokernel.π S.f ≫ ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom = Cofork.π cf
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
have : cg.ι ≫ cf.π = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom := by
  have eq₁ := IsLimit.conePointUniqueUpToIso_inv_comp (kernelIsKernel S.g) hg (.zero)
  have eq₂ := IsColimit.comp_coconePointUniqueUpToIso_hom (cokernelIsCokernel S.f) hf (.one)
  dsimp at eq₁ eq₂
  rw [← eq₁, ← eq₂, Category.assoc]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
let e₂ := IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
have eq₂ := IsColimit.comp_coconePointUniqueUpToIso_hom (cokernelIsCokernel S.f) hf (.one)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
eq₂ :
  (Cofork.ofπ (cokernel.π S.f) ⋯).ι.app WalkingParallelPair.one ≫
      ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom =
    cf.ι.app WalkingParallelPair.one
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
⊢ S.Exact ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
rw [exact_iff_kernel_ι_comp_cokernel_π_zero]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
let e₁ := IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
  IsIso.comp_right_eq_zero _ e₂.hom]

Result:
no goals