awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
rw :
  Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ cokernel.π (image.ι f))) 0
⊢ Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0
have rw₁ : Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
Tactic: rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
rw :
  Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ cokernel.π (image.ι f))) 0
rw₁ : Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
⊢ Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0
have rw₂ : Eq.{v + 1} (α := X ⟶ cokernel (X := image f) (image.ι f)) 0 0
Tactic: rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
⊢ CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      ((fun (x : Cofork f 0) ↦
          (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
        s) =
    s.π
have rw : Eq.{v + 1} (α := Y ⟶ s.pt)
  (CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 sorry))
    (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 sorry))
    ((fun (x : Cofork f 0) ↦
        (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 sorry) ⟶ x.pt))
      s))
  0
Tactic: rw [hf _ _ (CokernelCofork.condition s), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
rw :
  Eq.{v + 1} (α := Y ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      ((fun (x : Cofork f 0) ↦
          (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
        s))
    0
⊢ CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      ((fun (x : Cofork f 0) ↦
          (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
        s) =
    s.π
have rw₁ : Eq.{v + 1} (α := Y ⟶ s.pt) 0 0
Tactic: rw [hf _ _ (CokernelCofork.condition s), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h_1 : i.hom ≫ l = f
s_1 : CokernelCofork f
hs : IsColimit s_1
s : Cofork l 0
m : Cocone.pt (F := parallelPair l 0) (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ≫ m = s.π
⊢ m = (fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π ⋯) : s_1.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s
have apply : Cofork.π s_1 ≫ m =
  Cofork.π s_1 ≫
    (fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π sorry) : s_1.pt ⟶ (CokernelCofork.ofπ s.π sorry).pt)) s
Tactic: apply Cofork.IsColimit.hom_ext hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
j : WalkingParallelPair
⊢ s.ι.app j ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) j
have zero : s.ι.app zero ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l sorry)) zero
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
j : WalkingParallelPair
zero :
  s.ι.app WalkingParallelPair.zero ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) WalkingParallelPair.zero
⊢ s.ι.app j ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) j
have one : s.ι.app one ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l sorry)) one
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) zero
have zero : s.ι.app zero ≫ i.hom = f ≫ l
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = f ≫ l
have zero : s.ι.app zero ≫ i.hom = f ≫ Cofork.π s ≫ i.hom
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ Eq (α := G.obj Z ⟶ kernel (G.map f))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (G.map (kernel.lift f h w)) (kernelComparison f G))
    (kernel.lift (G.map f) (G.map h) ⋯)
have h₁ : CategoryStruct.comp (Y := equalizer (G.map f) 0)
    (CategoryStruct.comp (Y := G.obj (kernel f)) (G.map (kernel.lift f h w)) (kernelComparison f G))
    (equalizer.ι (G.map f) 0) =
  CategoryStruct.comp (Y := equalizer (G.map f) 0) (kernel.lift (G.map f) (G.map h) sorry) (equalizer.ι (G.map f) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) 0
have rw : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f ≫ f)) 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f ≫ f)) 0
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) 0
have rw₁ : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map 0) 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f ≫ f)) 0
rw₁ : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map 0) 0
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj (kernel f) ⟶ G.obj Y) 0 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g) ≫ G.map g) 0
have rw : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g ≫ g)) 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g ≫ g)) 0
⊢ Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g) ≫ G.map g) 0
have rw₁ : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map 0) 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g ≫ g)) 0
rw₁ : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map 0) 0
⊢ Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g) ≫ G.map g) 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj (kernel g) ⟶ G.obj Y') 0 0
Tactic: rw [← G.map_comp, kernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f) ≫ G.map p)
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (G.map (kernel.ι g)))
have simp : Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f ≫ p))
  (G.map (CategoryStruct.comp (Y := kernel g) (kernel.map f g p q hpq) (kernel.ι g)))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ Eq (α := cokernel (G.map f) ⟶ G.obj Z)
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.desc f h w)))
    (cokernel.desc (G.map f) (G.map h) ⋯)
have h₁ : CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0)
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.desc f h w))) =
  CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0) (cokernel.desc (G.map f) (G.map h) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map 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.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (coequalizer.π f 0)) 0
have rw : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map (f ≫ coequalizer.π f 0)) 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map (f ≫ coequalizer.π f 0)) 0
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (coequalizer.π f 0)) 0
have rw₁ : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map 0) 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map (f ≫ coequalizer.π f 0)) 0
rw₁ : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map 0) 0
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (coequalizer.π f 0)) 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj X ⟶ G.obj (cokernel f)) 0 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map g ≫ G.map (coequalizer.π g 0)) 0
have rw : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map (g ≫ coequalizer.π g 0)) 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map (g ≫ coequalizer.π g 0)) 0
⊢ Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map g ≫ G.map (coequalizer.π g 0)) 0
have rw₁ : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map 0) 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map (g ≫ coequalizer.π g 0)) 0
rw₁ : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map 0) 0
⊢ Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map g ≫ G.map (coequalizer.π g 0)) 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj X' ⟶ G.obj (cokernel g)) 0 0
Tactic: rw [← G.map_comp, cokernel.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (G.map (coequalizer.π f 0)) (G.map (cokernel.map f g p q hpq)))
    (G.map q ≫ G.map (coequalizer.π g 0))
have simp : Eq (α := G.obj Y ⟶ G.obj (cokernel g))
  (G.map (CategoryStruct.comp (Y := cokernel f) (coequalizer.π f 0) (cokernel.map f g p q hpq)))
  (G.map (q ≫ coequalizer.π g 0))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ k = J.snd default
have this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
Tactic: have := h.symm.le (Set.mem_univ k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
⊢ k = J.snd default
have this₁ : k = J.fst default ∨ k = J.snd default
Tactic: push _ ∈ _ at this
Cleared hypotheses: this