[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ G.map (Fork.ι c) ≫ G.map f = 0
[PROOFSTEP]
rw [← G.map_comp, c.condition, G.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ IsLimit (G.mapCone c) ≃ IsLimit (map c G)
[PROOFSTEP]
refine' (IsLimit.postcomposeHomEquiv _ _).symm.trans (IsLimit.equivIsoLimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
[PROOFSTEP]
refine' parallelPair.ext (Iso.refl _) (Iso.refl _) _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (Cones.postcompose
          (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
              (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
              (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
      (G.mapCone c) ≅
    map c G
[PROOFSTEP]
exact Cones.ext (Iso.refl _) (by rintro (_ | _) <;> aesop_cat)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app
        ((Cones.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
            (G.mapCone c)).π
        j =
      (Iso.refl
            ((Cones.postcompose
                    (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                        (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                        (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
                (G.mapCone c)).pt).hom ≫
        NatTrans.app (map c G).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
      ((Cones.postcompose
              (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                  (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                  (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                  (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
          (G.mapCone c)).π
      WalkingParallelPair.zero =
    (Iso.refl
          ((Cones.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
              (G.mapCone c)).pt).hom ≫
      NatTrans.app (map c G).π WalkingParallelPair.zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
      ((Cones.postcompose
              (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                  (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                  (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                  (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
          (G.mapCone c)).π
      WalkingParallelPair.one =
    (Iso.refl
          ((Cones.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
              (G.mapCone c)).pt).hom ≫
      NatTrans.app (map c G).π WalkingParallelPair.one
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasZeroMorphisms C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms D
G : C ⥤ D
inst✝¹ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝ : PreservesLimit (parallelPair f 0) G
l : IsLimit (KernelFork.ofι h w)
⊢ G.map h ≫ G.map f = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ G.map (kernel.ι f) ≫ G.map f = G.map (kernel.ι f) ≫ 0
[PROOFSTEP]
simp only [← G.map_comp, kernel.condition, comp_zero, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ PreservesLimit (parallelPair f 0) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (kernelIsKernel f)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (G.mapCone (Fork.ofι (kernel.ι f) (_ : kernel.ι f ≫ f = kernel.ι f ≫ 0)))
[PROOFSTEP]
apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (KernelFork.ofι (G.map (kernel.ι f)) (_ : G.map (kernel.ι f) ≫ G.map f = 0))
[PROOFSTEP]
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (kernelIsKernel (G.map f)) i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom = kernelComparison f G
[PROOFSTEP]
rw [← cancel_mono (kernel.ι _)]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)
[PROOFSTEP]
simp [PreservesKernel.iso]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ IsIso (kernelComparison f G)
[PROOFSTEP]
rw [← PreservesKernel.iso_hom]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ IsIso (PreservesKernel.iso G f).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, hpq, G.map_comp]
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (_ : G.map f ≫ G.map q = G.map p ≫ G.map g) ≫
      (PreservesKernel.iso G g).inv =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq)
[PROOFSTEP]
rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp, PreservesKernel.iso_hom,
  kernelComparison_comp_kernel_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ G.map f ≫ G.map (Cofork.π c) = 0
[PROOFSTEP]
rw [← G.map_comp, c.condition, G.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (map c G)
[PROOFSTEP]
refine' (IsColimit.precomposeHomEquiv _ _).symm.trans (IsColimit.equivIsoColimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G
[PROOFSTEP]
refine' parallelPair.ext (Iso.refl _) (Iso.refl _) _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (Cocones.precompose
          (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
              (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
              (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
      (G.mapCocone c) ≅
    map c G
[PROOFSTEP]
exact Cocones.ext (Iso.refl _) (by rintro (_ | _) <;> aesop_cat)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).ι
          j ≫
        (Iso.refl
            ((Cocones.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                        (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                        (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
                (G.mapCocone c)).pt).hom =
      NatTrans.app (map c G).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
        ((Cocones.precompose
                (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
            (G.mapCocone c)).ι
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).pt).hom =
    NatTrans.app (map c G).ι WalkingParallelPair.zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
        ((Cocones.precompose
                (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
            (G.mapCocone c)).ι
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).pt).hom =
    NatTrans.app (map c G).ι WalkingParallelPair.one
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasZeroMorphisms C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms D
G : C ⥤ D
inst✝¹ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝ : PreservesColimit (parallelPair f 0) G
l : IsColimit (CokernelCofork.ofπ h w)
⊢ G.map f ≫ G.map h = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ G.map f ≫ G.map (cokernel.π f) = 0 ≫ G.map (cokernel.π f)
[PROOFSTEP]
simp only [← G.map_comp, cokernel.condition, zero_comp, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ PreservesColimit (parallelPair f 0) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (cokernelIsCokernel f)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0 ≫ cokernel.π f)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (CokernelCofork.ofπ (G.map (cokernel.π f)) (_ : G.map f ≫ G.map (cokernel.π f) = 0))
[PROOFSTEP]
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (cokernelIsCokernel (G.map f)) i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G
[PROOFSTEP]
rw [← cancel_epi (cokernel.π _)]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
[PROOFSTEP]
simp [PreservesCokernel.iso]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (cokernelComparison f G)
[PROOFSTEP]
rw [← PreservesCokernel.iso_inv]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (PreservesCokernel.iso G f).inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, hpq, G.map_comp]
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫
      cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (_ : G.map f ≫ G.map q = G.map p ≫ G.map g) =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom
[PROOFSTEP]
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
  cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
have := KernelFork.IsLimit.isIso_ι c hc rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
refine' (KernelFork.isLimitMapConeEquiv c G).symm _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (KernelFork.map c G)
[PROOFSTEP]
refine' IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ KernelFork.ofι (𝟙 (G.obj X)) (_ : 𝟙 (G.obj X) ≫ G.map 0 = 0) ≅ KernelFork.map c G
[PROOFSTEP]
exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ (G.mapIso (asIso (Fork.ι c))).symm.hom ≫ Fork.ι (KernelFork.map c G) =
    Fork.ι (KernelFork.ofι (𝟙 (G.obj X)) (_ : 𝟙 (G.obj X) ≫ G.map 0 = 0))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
have := CokernelCofork.IsColimit.isIso_π c hc rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
refine' (CokernelCofork.isColimitMapCoconeEquiv c G).symm _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (CokernelCofork.map c G)
[PROOFSTEP]
refine' IsColimit.ofIsoColimit (CokernelCofork.IsColimit.ofId _ (G.map_zero _ _)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ CokernelCofork.ofπ (𝟙 (G.obj Y)) (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 0) ≅ CokernelCofork.map c G
[PROOFSTEP]
exact (Cofork.ext (G.mapIso (asIso (Cofork.π c))) (by simp))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ Cofork.π (CokernelCofork.ofπ (𝟙 (G.obj Y)) (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 0)) ≫ (G.mapIso (asIso (Cofork.π c))).hom =
    Cofork.π (CokernelCofork.map c G)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair f 0) G
[PROOFSTEP]
rw [hf]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair 0 0) G
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair f 0) G
[PROOFSTEP]
rw [hf]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair 0 0) G
[PROOFSTEP]
infer_instance
