-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories which preserves kernels preserves all finite limits.
-/
lemma preservesFiniteLimits_of_preservesKernels [HasFiniteProducts C] [HasEqualizers C]
    [HasZeroObject C] [HasZeroObject D] [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] :
    PreservesFiniteLimits 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
⊢ PreservesFiniteLimits F

Tactic:
letI := preservesLimitsOfShape_pempty_of_preservesTerminal 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝¹ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this✝ : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) F := preservesLimitsOfShape_pempty_of_preservesTerminal F
⊢ PreservesFiniteLimits 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
⊢ PreservesFiniteLimits F

Tactic:
letI := preservesTerminalObject_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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
⊢ PreservesFiniteLimits 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝² : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this✝¹ : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
this✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F := preservesLimitsOfShape_pempty_of_preservesTerminal F
this : PreservesFiniteProducts F :=
  { preserves := fun x => preservesFiniteProducts_of_preserves_binary_and_terminal F (Fin x) }
⊢ PreservesFiniteLimits F

Tactic:
exact preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesFiniteLimits F

Tactic:
letI := preservesEqualizers_of_preservesKernels 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
⊢ PreservesFiniteLimits 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝¹ : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this✝ : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) F := preservesLimitsOfShape_pempty_of_preservesTerminal F
⊢ PreservesFiniteLimits F

Tactic:
letI : PreservesFiniteProducts F :=
  ⟨fun _ ↦ preservesFiniteProducts_of_preserves_binary_and_terminal 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✝⁴ : HasFiniteProducts C
inst✝³ : HasEqualizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝² : PreservesLimitsOfShape WalkingParallelPair F := preservesEqualizers_of_preservesKernels F
this✝¹ : PreservesLimit (empty C) F := preservesTerminalObject_of_preservesZeroMorphisms F
this✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F := preservesLimitsOfShape_pempty_of_preservesTerminal F
this : PreservesFiniteProducts F :=
  { preserves := fun x => preservesFiniteProducts_of_preserves_binary_and_terminal F (Fin x) }
⊢ PreservesFiniteLimits F