awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : HasEqualizers.{v₁, u₁} A
inst_3 : HasImages.{v₁, u₁} A
inst_4 : StrongEpiCategory.{v₂, u₂} B
inst_5 : HasImages.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_6 : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst_7 : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ Eq (α := L.obj (image f) ⟶ L.obj Y)
    (CategoryStruct.comp (Y := image (L.map f)) (Iso.inv (iso L f) : L.obj (image f) ⟶ image (L.map f))
        (image.ι (L.map f) : image (L.map f) ⟶ L.obj Y) :
      L.obj (image f) ⟶ L.obj Y)
    (L.map (image.ι f) : L.obj (image f) ⟶ L.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
rw : G.map (Fork.ι c ≫ f) = 0
rw₁ : Eq (α := G.obj c.pt ⟶ G.obj Y) (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj c.pt ⟶ G.obj Y) 0 0
⊢ G.map (Fork.ι c) ≫ G.map f = 0

Tactic:
rw [← G.map_comp, c.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ Fork.ι (c.map G) = G.map (Fork.ι c)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 : parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
refine_2 :
  (Cone.postcompose
          (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
      (G.mapCone c) ≅
    c.map G
⊢ IsLimit (G.mapCone c) ≃ IsLimit (F := parallelPair (G.map f) 0) (c.map G)

Tactic:
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.trans, CategoryTheory.Limits.IsLimit.equivIsoLimit, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 :
  (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left
refine_1₁ :
  (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right
⊢ parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0

Tactic:
refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (Cone.postcompose
          (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
      (G.mapCone c) ≅
    c.map G

Tactic:
exact Cone.ext (Iso.refl _) (by rintro (_ | _) <;> cat_disch)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : PreservesLimit (parallelPair f 0) G
l : IsLimit (KernelFork.ofι h w)
⊢ G.map h ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : PreservesLimit (parallelPair f 0) G
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) (G.map (kernel.ι f) ≫ 0)

Tactic:
simp only [← G.map_comp, kernel.condition, comp_zero, Functor.map_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
i : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
apply : IsLimit (F := parallelPair f 0 ⋙ G) (G.mapCone (Fork.ofι (P := kernel f) (kernel.ι f) ⋯))
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
i : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
apply : IsLimit (F := parallelPair (G.map f) 0) (KernelFork.ofι (Z := G.obj (kernel f)) (G.map (kernel.ι f)) ⋯)
⊢ IsLimit (F := parallelPair f 0 ⋙ G) (G.mapCone (Fork.ofι (P := kernel f) (kernel.ι f) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _

Premises used: CategoryTheory.Limits.isLimitMapConeForkEquiv', CategoryTheory.Limits.kernel.condition, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
i : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
⊢ IsLimit (F := parallelPair (G.map f) 0) (KernelFork.ofι (Z := G.obj (kernel f)) (G.map (kernel.ι f)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (kernelIsKernel (G.map f)) i

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
⊢ Eq (α := kernel (G.map f) ⟶ G.obj X)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (iso G f)) (G.map (kernel.ι f))) (kernel.ι (G.map f))

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp (isLimitOfHasKernelOfPreservesLimit G f)
    (limit.isLimit _) (WalkingParallelPair.zero)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
rw :
  Eq (α := G.obj (kernel f) ⟶ G.obj X)
    (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (iso G f)) (kernel.ι (G.map f)))
    (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G) (kernel.ι (G.map f)))
⊢ Eq (α := G.obj (kernel f) ⟶ kernel (G.map f)) (Iso.hom (iso G f)) (kernelComparison f G)

Tactic:
rw [← cancel_mono (kernel.ι _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X)
    (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (iso G f)) (kernel.ι (G.map f)))
    (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G) (kernel.ι (G.map f)))

Tactic:
simp [PreservesKernel.iso]

Premises used: CategoryTheory.Limits.PreservesKernel.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
rw : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
⊢ IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)

Tactic:
rw [← PreservesKernel.iso_hom]

Premises used: CategoryTheory.Limits.PreservesKernel.iso_hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
⊢ IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasKernel g
inst_9 : HasKernel (G.map g)
inst_10 : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : G.map (f ≫ q) = G.map p ≫ G.map g
rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
rw₂ rw₃ : G.map p ≫ G.map g = G.map p ≫ G.map g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
rw : G.map (f ≫ Cofork.π c) = 0
rw₁ : Eq (α := G.obj X ⟶ G.obj c.pt) (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj X ⟶ G.obj c.pt) 0 0
⊢ G.map f ≫ G.map (Cofork.π c) = 0

Tactic:
rw [← G.map_comp, c.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ Cofork.π (c.map G) = G.map (Cofork.π c)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 : parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G
refine_2 :
  (Cocone.precompose
          (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
      (G.mapCocone c) ≅
    c.map G
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (F := parallelPair (G.map f) 0) (c.map G)

Tactic:
refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)

Premises used: Equiv.trans, CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 :
  (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left
refine_1₁ :
  (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right
⊢ parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G

Tactic:
refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ (Cocone.precompose
          (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
      (G.mapCocone c) ≅
    c.map G

Tactic:
exact Cocone.ext (Iso.refl _) (by rintro (_ | _) <;> cat_disch)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst_5 : PreservesColimit (parallelPair f 0) G
l : IsColimit (CokernelCofork.ofπ h w)
⊢ G.map f ≫ G.map h = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst_5 : HasCokernel f
inst_6 : PreservesColimit (parallelPair f 0) G
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (cokernel.π f)) (0 ≫ G.map (cokernel.π f))

Tactic:
simp only [← G.map_comp, cokernel.condition, zero_comp, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
i : IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (cokernelComparison f G)
apply : IsColimit (F := parallelPair f 0 ⋙ G) (G.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
i : IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (cokernelComparison f G)
apply :
  IsColimit (F := parallelPair (G.map f) 0) (CokernelCofork.ofπ (Z := G.obj (cokernel f)) (G.map (cokernel.π f)) ⋯)
⊢ IsColimit (F := parallelPair f 0 ⋙ G) (G.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))

Tactic:
apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _

Premises used: CategoryTheory.Limits.cokernel.condition, Equiv.symm, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv', DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
i : IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (cokernelComparison f G)
⊢ IsColimit (F := parallelPair (G.map f) 0) (CokernelCofork.ofπ (Z := G.obj (cokernel f)) (G.map (cokernel.π f)) ⋯)

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (cokernelIsCokernel (G.map f)) i

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.IsColimit.ofPointIso