-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories preserves the equalizer of two
morphisms if it preserves all kernels. -/
lemma preservesEqualizer_of_preservesKernels
    [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F]
    {X Y : C} (f g : X ⟶ Y) : PreservesLimit (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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesLimit (parallelPair f g) F

Tactic:
letI := preservesBinaryBiproducts_of_preservesBinaryProducts 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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
⊢ PreservesLimit (parallelPair f g) F

Proof state:
case preserves
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (kernelForkOfFork (Fork.ofι (Fork.ι c) ⋯)) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
dsimp only [kernelForkOfFork_ofι] at c'

Result:
case preserves
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
⊢ Nonempty (IsLimit (F.mapCone 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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ (Iso.refl (forkOfKernelFork ((Cones.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).pt).hom ≫
      (Fork.ofι (F.map (Fork.ι c)) ⋯).ι =
    (forkOfKernelFork ((Cones.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).ι

Tactic:
simp [p]

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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
⊢ PreservesLimit (parallelPair f g) F

Tactic:
constructor

Result:
case preserves
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
⊢ ∀ {c : Cone (parallelPair f g)}, IsLimit c → Nonempty (IsLimit (F.mapCone 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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)

Tactic:
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.eqOfHomEq F.map_sub rfl

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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)

Proof state:
case preserves
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
⊢ ∀ {c : Cone (parallelPair f g)}, IsLimit c → Nonempty (IsLimit (F.mapCone c))

Tactic:
intro c i

Result:
case preserves
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))