-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories which preserves kernels preserves all finite limits.
-/
lemma preservesFiniteColimits_of_preservesCokernels [HasFiniteCoproducts C] [HasCoequalizers C]
    [HasZeroObject C] [HasZeroObject D]
    [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] : PreservesFiniteColimits 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝² : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝¹ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
this : PreservesFiniteCoproducts F :=
  { preserves := fun x => preservesFiniteCoproductsOfPreservesBinaryAndInitial F (Fin x) }
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
⊢ PreservesFiniteColimits F

Tactic:
letI := preservesInitialObject_of_preservesZeroMorphisms 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
⊢ PreservesFiniteColimits 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
⊢ PreservesFiniteColimits F

Tactic:
letI := preservesColimitsOfShape_pempty_of_preservesInitial 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
⊢ PreservesFiniteColimits 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
⊢ PreservesFiniteColimits F

Tactic:
letI : PreservesFiniteCoproducts F :=
  ⟨fun _ ↦ preservesFiniteCoproductsOfPreservesBinaryAndInitial 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝² : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝¹ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
this : PreservesFiniteCoproducts F :=
  { preserves := fun x => preservesFiniteCoproductsOfPreservesBinaryAndInitial F (Fin x) }
⊢ PreservesFiniteColimits 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ PreservesFiniteColimits F

Tactic:
letI := preservesCoequalizers_of_preservesCokernels 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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
⊢ PreservesFiniteColimits F