awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
w :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := image f) (factorThruImage f)
          (IsImage.lift (Image.isImage f) (imageStrongEpiMonoFactorisation f).toMonoFactorisation) :
        X ⟶ Abelian.image f)
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₁ :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
        (image.lift (imageStrongEpiMonoFactorisation f).toMonoFactorisation) ≫
      equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₂ :
  (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₃ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ Iso.inv (imageIsoImage f)) (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
have w₄ : CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
    (equalizer.ι (cokernel.π f) 0) =
  CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
        (kernel.lift (cokernel.π f) (Limits.image.ι f) sorry) (equalizer.ι (cokernel.π f) 0) :
      image f ⟶ Y)
Tactic: rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
    imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
    kernel.lift_ι, Limits.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
w :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := image f) (factorThruImage f)
          (IsImage.lift (Image.isImage f) (imageStrongEpiMonoFactorisation f).toMonoFactorisation) :
        X ⟶ Abelian.image f)
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₁ :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
        (image.lift (imageStrongEpiMonoFactorisation f).toMonoFactorisation) ≫
      equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₂ :
  (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₃ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₄ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0) :
        image f ⟶ Y)
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ Iso.inv (imageIsoImage f)) (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
have w₅ : f =
  CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
        (kernel.lift (cokernel.π f) (Limits.image.ι f) sorry) (equalizer.ι (cokernel.π f) 0) :
      image f ⟶ Y)
Tactic: rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
    imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
    kernel.lift_ι, Limits.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
w :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := image f) (factorThruImage f)
          (IsImage.lift (Image.isImage f) (imageStrongEpiMonoFactorisation f).toMonoFactorisation) :
        X ⟶ Abelian.image f)
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₁ :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
        (image.lift (imageStrongEpiMonoFactorisation f).toMonoFactorisation) ≫
      equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₂ :
  (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₃ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₄ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0) :
        image f ⟶ Y)
w₅ :
  f =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0) :
        image f ⟶ Y)
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ Iso.inv (imageIsoImage f)) (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
have w₆ : f =
  CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
    (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
        (kernel.lift (cokernel.π f) (Limits.image.ι f) sorry) (kernel.ι (cokernel.π f)) :
      image f ⟶ Y)
Tactic: rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
    imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
    kernel.lift_ι, Limits.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
⊢ IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F) (F.mapCone (KernelFork.ofι i ⋯))
have refine : IsLimit ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i sorry)))
Tactic: refine IsLimit.postcomposeInvEquiv e _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ IsLimit ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯)))
have refine : Iso.hom
      (Iso.refl
        (Cone.pt (F :=
          parallelPair (Y :=
            Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) sorry))
            (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) sorry)) 0)
          (KernelFork.ofι (F.map i) sorry))) ≫
    Fork.ι ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i sorry))) =
  Fork.ι (KernelFork.ofι (F.map i) sorry)
Tactic: refine IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (Y :=
              Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
              (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
            (KernelFork.ofι (F.map i) ⋯))) ≫
      Fork.ι ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯))) =
    Fork.ι (KernelFork.ofι (F.map i) ⋯)
have change : 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i
Tactic: change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i
have rw : 𝟙 (F.obj X) ≫ F.map i = F.map i
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
rw : 𝟙 (F.obj X) ≫ F.map i = F.map i
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i
have rw₁ : F.map i = F.map i
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F) (F.mapCocone (CokernelCofork.ofπ p ⋯))
have refine : IsColimit ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p sorry)))
Tactic: refine IsColimit.precomposeInvEquiv e _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ IsColimit ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))
have refine : Cofork.π (CokernelCofork.ofπ (F.map p) sorry) ≫
    Iso.hom
      (Iso.refl
        (Cocone.pt (F :=
          parallelPair (X :=
            Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) sorry))
            (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) sorry)) 0)
          (CokernelCofork.ofπ (F.map p) sorry))) =
  Cofork.π ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p sorry)))
Tactic: refine IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ Cofork.π (CokernelCofork.ofπ (F.map p) ⋯) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            parallelPair (X :=
              Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
              (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
            (CokernelCofork.ofπ (F.map p) ⋯))) =
    Cofork.π ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))
have change : F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p
Tactic: change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p
have rw : F.map p = 𝟙 (F.obj X) ≫ F.map p
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
rw : F.map p = 𝟙 (F.obj X) ≫ F.map p
⊢ F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p
have rw₁ : F.map p = F.map p
Tactic: rw [Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback f g ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) (biprod.desc f (-g)) : pullback f g ⟶ Z)
    (0 : pullback f g ⟶ Z)
have rw : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (pullback.snd f g ≫ (-g)) = 0
Tactic: rw [biprod.lift_desc, comp_neg, pullback.condition, add_neg_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (pullback.snd f g ≫ (-g)) = 0
⊢ Eq (α := pullback f g ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) (biprod.desc f (-g)) : pullback f g ⟶ Z)
    (0 : pullback f g ⟶ Z)
have rw₁ : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (-pullback.snd f g ≫ g) = 0
Tactic: rw [biprod.lift_desc, comp_neg, pullback.condition, add_neg_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
rw : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (pullback.snd f g ≫ (-g)) = 0
rw₁ : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (-pullback.snd f g ≫ g) = 0
⊢ Eq (α := pullback f g ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) (biprod.desc f (-g)) : pullback f g ⟶ Z)
    (0 : pullback f g ⟶ Z)
have rw₂ : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.snd f g ≫ g) (-pullback.snd f g ≫ g) = 0
Tactic: rw [biprod.lift_desc, comp_neg, pullback.condition, add_neg_cancel]