awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
have rw₂ : G.map p ≫ G.map g = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw : Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
  (CategoryStruct.comp (Y := G.obj (kernel g))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
    (Iso.hom (PreservesKernel.iso G g)))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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 :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw₁ : Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
  (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (Iso.hom (PreservesKernel.iso G g))))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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 :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
rw₁ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq))
        (Iso.hom (PreservesKernel.iso G g))))
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw₂ : Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
  (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G)))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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 :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
rw₁ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq))
        (Iso.hom (PreservesKernel.iso G g))))
rw₂ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G)))
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw₃ : Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
  (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
    (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry))
  (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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 :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
rw₁ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq))
        (Iso.hom (PreservesKernel.iso G g))))
rw₂ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G)))
rw₃ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
      (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw₄ : Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
  (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G)
    (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry))
  (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
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 :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel g))
      (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
      (Iso.hom (PreservesKernel.iso G g)))
rw₁ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq))
        (Iso.hom (PreservesKernel.iso G g))))
rw₂ :
  Eq (α := kernel (G.map f) ⟶ kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f))
      (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G)))
rw₃ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
      (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
rw₄ :
  Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
    (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G)
      (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
⊢ Eq (α := kernel (G.map f) ⟶ G.obj (kernel g))
    (CategoryStruct.comp (Y := kernel (G.map g)) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesKernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (Iso.inv (PreservesKernel.iso G f)) (G.map (kernel.map f g p q hpq)))
have rw₅ : Eq (α := G.obj (kernel f) ⟶ kernel (G.map g))
  (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
  (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (kernelComparison g G))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
    PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ G.map f ≫ G.map (Cofork.π c) = 0
have rw : G.map (f ≫ Cofork.π c) = 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ G.map f ≫ G.map (Cofork.π c) = 0
have rw₁ : Eq (α := G.obj X ⟶ G.obj c.pt) (G.map 0) 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ G.map f ≫ G.map (Cofork.π c) = 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj X ⟶ G.obj c.pt) 0 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (F := parallelPair (G.map f) 0) (c.map G)
have refine_1 : parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G
Tactic: refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (F := parallelPair (G.map f) 0) (c.map G)
have 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)) sorry sorry).hom).obj
    (G.mapCocone c) ≅
  c.map G
Tactic: refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 ≅ parallelPair f 0 ⋙ G
have 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
Tactic: refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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
⊢ parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G
have 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
Tactic: refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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)
⊢ PreservesColimit (parallelPair f 0) G
have apply : IsColimit (F := parallelPair f 0 ⋙ G) (G.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) sorry))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 f 0 ⋙ G) (G.mapCocone (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯))
have apply : IsColimit (F := parallelPair (G.map f) 0) (CokernelCofork.ofπ (Z := G.obj (cokernel f)) (G.map (cokernel.π f)) sorry)
Tactic: apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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)
inst_7 : PreservesColimit (parallelPair f 0) G
⊢ Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel f)) (Iso.inv (iso G f)) (cokernelComparison f G)
have rw : Eq (α := G.obj Y ⟶ G.obj (cokernel f))
  (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (Iso.inv (iso G f)))
  (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (cokernelComparison f G))
Tactic: rw [← cancel_epi (cokernel.π _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
⊢ IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (cokernelComparison f G)
have rw : IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
Tactic: rw [← PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : 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
have rw : G.map (f ≫ q) = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (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
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
have rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
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 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (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
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
have rw₂ : G.map p ≫ G.map g = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]