awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
        (σ : Limits.prod.{v, u} X X ⟶ X) ≫
      g =
    g
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    g
have rw₁ : 𝟙 X ≫ g = g
Tactic: rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
        (σ : Limits.prod.{v, u} X X ⟶ X) ≫
      g =
    g
rw₁ : 𝟙 X ≫ g = g
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
    g
have rw₂ : g = g
Tactic: rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
⊢ f = g
have f₁ : f =
  f ≫
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y)
Tactic: calc
    f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
    _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
    _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
    _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
f₁ :
  f =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)
⊢ f = g
have f₂ : f ≫
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y))
Tactic: calc
    f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
    _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
    _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
    _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
f₁ :
  f =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)
f₂ :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y))
⊢ f = g
have f₃ : CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
    (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
Tactic: calc
    f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
    _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
    _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
    _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
f : X ⟶ Y
g :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := Limits.prod.{v, u} X X) (diag X) 0)
      (CokernelCofork.ofπ σ ⋯ : CokernelCofork.{v, u} (Y := Limits.prod.{v, u} X X) (diag X)) ⟶
    Y
hg :
  Eq (α := Limits.prod.{v, u} X X ⟶ Y) (Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g : Limits.prod.{v, u} X X ⟶ Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) :
      Limits.prod.{v, u} X X ⟶ Y)
f₁ :
  f =
    f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)
f₂ :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y))
f₃ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map f f : Limits.prod.{v, u} X X ⟶ Limits.prod.{v, u} Y Y) (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
      (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y)
⊢ f = g
have f₄ : CategoryStruct.comp (Y := Limits.prod.{v, u} X X) (prod.lift (𝟙 X) 0 : X ⟶ Limits.prod.{v, u} X X)
    (σ ≫ g : Limits.prod.{v, u} X X ⟶ Y) =
  g
Tactic: calc
    f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
    _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
    _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
    _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ a - 0 = a
have rw : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  a
Tactic: rw [sub_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)
have a₁ : prod.lift a 0
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : prod.lift a 0
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)
have a₂ : (σ : Limits.prod.{v, u} Y Y ⟶ Y)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| prod.lift a 0
have a₁ : a
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a
| prod.lift a 0
have congr : 0
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| a
have a₁ : a ≫ 𝟙 Y
Tactic: rw [← Category.comp_id a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| 0
have rw : a ≫ 0
Tactic: rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)
have a₁ : a ≫ 𝟙 Y
Tactic: congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a ≫ 𝟙 Y
| CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y)
have a₂ : (σ : Limits.prod.{v, u} Y Y ⟶ Y)
Tactic: congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
have conv_lhs : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  a
Tactic: conv_lhs =>
    congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
have rw : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) 0 : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  a
Tactic: rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
have rw₁ : a ≫
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  a
Tactic: rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
rw₁ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
have rw₂ : a ≫ 𝟙 Y = a
Tactic: rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) 0 : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
rw₁ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) 0 : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
rw₂ : a ≫ 𝟙 Y = a
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 0) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a
have rw₃ : a = a
Tactic: rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
⊢ a - a = 0
have rw : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
⊢ a - a = 0
have rw₁ : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
⊢ a - a = 0
have rw₂ : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) (𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
    (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) (𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
⊢ a - a = 0
have rw₃ : a ≫
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) (𝟙 Y) : Y ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
  0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) (𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₃ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) (𝟙 Y) : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
⊢ a - a = 0
have rw₄ : Eq (α := X ⟶ Y) (a ≫ 0) 0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a a : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (a ≫ 𝟙 Y) (a ≫ 𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (a ≫ prod.lift (𝟙 Y) (𝟙 Y) : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₃ :
  a ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (𝟙 Y) (𝟙 Y) : Y ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    0
rw₄ : Eq (α := X ⟶ Y) (a ≫ 0) 0
⊢ a - a = 0
have rw₅ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
⊢ HSub.hSub (α := X ⟶ Limits.prod.{v, u} Y Y) (prod.lift a b) (prod.lift c d) = prod.lift (a - c) (b - d)
have simp : Eq (α := X ⟶ Limits.prod.{v, u} Y Y)
  (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
    (prod.lift (prod.lift a b) (prod.lift c d) :
      X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
    (σ : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y))
  (prod.lift
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y))
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
Tactic: simp only [sub_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
⊢ Eq (α := X ⟶ Limits.prod.{v, u} Y Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (prod.lift (prod.lift a b) (prod.lift c d) :
        X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (σ : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y))
    (prod.lift
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y))
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
have h₁ : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (prod.lift (prod.lift a b) (prod.lift c d) :
        X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (σ : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y))
    prod.fst =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
    (prod.lift
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y))
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
    prod.fst
Tactic: ext