-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories preserves the coequalizer of two
morphisms if it preserves all cokernels. -/
lemma preservesCoequalizer_of_preservesCokernels
    [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] {X Y : C} (f g : X ⟶ Y) :
    PreservesColimit (parallelPair f g) F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) ⋯)

Tactic:
exact
  IsColimit.ofIsoColimit
    (isColimitCoforkOfCokernelCofork ((IsColimit.precomposeHomEquiv p.symm _).symm iFc))
    (Cofork.ext (Iso.refl _) (by simp [p]))

Result:
no goals

Proof state:
case preserves.val
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ IsColimit (F.mapCocone c)

Tactic:
apply
  IsColimit.ofIsoColimit _ ((Cocones.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ IsColimit ((Cocones.functoriality (parallelPair f g) F).obj (Cofork.ofπ (Cofork.π c) ⋯))

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.right

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesColimit (parallelPair f g) F

Tactic:
letI := preservesBinaryBiproducts_of_preservesBinaryCoproducts F

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
⊢ PreservesColimit (parallelPair f g) F