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
a b : X ⟶ Y
rw : -(a - -b) = -a - b
rw₁ : -a + -b = -a - b
⊢ -(a + b) = -a - b
have rw₂ : -a - b = -a - b
Tactic: rw [add_def, neg_sub', add_neg]
-- 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 : X ⟶ Y
⊢ a - b + c = a - (b - c)
have rw : a - b - -c = a - (b - c)
Tactic: rw [add_def, neg_def, sub_sub_sub, sub_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 : X ⟶ Y
rw : a - b - -c = a - (b - c)
⊢ a - b + c = a - (b - c)
have rw₁ : a - b - (0 - c) = a - (b - c)
Tactic: rw [add_def, neg_def, sub_sub_sub, sub_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 : X ⟶ Y
rw : a - b - -c = a - (b - c)
rw₁ : a - b - (0 - c) = a - (b - c)
⊢ a - b + c = a - (b - c)
have rw₂ : a - 0 - (b - c) = a - (b - c)
Tactic: rw [add_def, neg_def, sub_sub_sub, sub_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 : X ⟶ Y
rw : a - b - -c = a - (b - c)
rw₁ : a - b - (0 - c) = a - (b - c)
rw₂ : a - 0 - (b - c) = a - (b - c)
⊢ a - b + c = a - (b - c)
have rw₃ : a - (b - c) = a - (b - c)
Tactic: rw [add_def, neg_def, sub_sub_sub, sub_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 : X ⟶ Y
| a + b + c
have a₁ : a + b
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 b c : X ⟶ Y
a₁ : a + b
| a + b + c
have a₂ : c
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 b c : X ⟶ Y
| a + b
have a₁ : a - -b
Tactic: rw [add_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 : X ⟶ Y
| a + b + c
have a₁ : a - -b
Tactic: congr; rw [add_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 : X ⟶ Y
a₁ : a - -b
| a + b + c
have a₂ : c
Tactic: congr; rw [add_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 : X ⟶ Y
⊢ a + b + c = a + (b + c)
have conv_lhs : a - -b + c = a + (b + c)
Tactic: conv_lhs =>
    congr; rw [add_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 : X ⟶ Y
⊢ a - -b + c = a + (b + c)
have rw : a - (-b - c) = a + (b + c)
Tactic: rw [sub_add, ← add_neg, neg_sub', neg_neg]
-- 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 : X ⟶ Y
rw : a - (-b - c) = a + (b + c)
⊢ a - -b + c = a + (b + c)
have rw₁ : a + -(-b - c) = a + (b + c)
Tactic: rw [sub_add, ← add_neg, neg_sub', neg_neg]
-- 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 : X ⟶ Y
rw : a - (-b - c) = a + (b + c)
rw₁ : a + -(-b - c) = a + (b + c)
⊢ a - -b + c = a + (b + c)
have rw₂ : a + (- -b + c) = a + (b + c)
Tactic: rw [sub_add, ← add_neg, neg_sub', neg_neg]
-- 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 : X ⟶ Y
rw : a - (-b - c) = a + (b + c)
rw₁ : a + -(-b - c) = a + (b + c)
rw₂ : a + (- -b + c) = a + (b + c)
⊢ a - -b + c = a + (b + c)
have rw₃ : a + (b + c) = a + (b + c)
Tactic: rw [sub_add, ← add_neg, neg_sub', neg_neg]
-- 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 : a - -0 = a
Tactic: rw [add_def, neg_def, sub_self, sub_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 : a - -0 = a
⊢ a + 0 = a
have rw₁ : a - HSub.hSub (α := X ⟶ Y) 0 0 = a
Tactic: rw [add_def, neg_def, sub_self, sub_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 : a - -0 = a
rw₁ : a - HSub.hSub (α := X ⟶ Y) 0 0 = a
⊢ a + 0 = a
have rw₂ : a - 0 = a
Tactic: rw [add_def, neg_def, sub_self, sub_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 : a - -0 = a
rw₁ : a - HSub.hSub (α := X ⟶ Y) 0 0 = a
rw₂ : a - 0 = a
⊢ a + 0 = a
have rw₃ : a = a
Tactic: rw [add_def, neg_def, sub_self, sub_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g - h) = f ≫ g - f ≫ h
have rw : f ≫
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift g h : Y ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  f ≫ g - f ≫ h
Tactic: rw [sub_def, ← Category.assoc, prod.comp_lift, 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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift g h : Y ⟶ Limits.prod.{v, u} Z Z)
        (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
⊢ f ≫ (g - h) = f ≫ g - f ≫ h
have rw₁ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (f ≫ prod.lift g h : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  f ≫ g - f ≫ h
Tactic: rw [sub_def, ← Category.assoc, prod.comp_lift, 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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift g h : Y ⟶ Limits.prod.{v, u} Z Z)
        (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (f ≫ prod.lift g h : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
⊢ f ≫ (g - h) = f ≫ g - f ≫ h
have rw₂ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ g) (f ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  f ≫ g - f ≫ h
Tactic: rw [sub_def, ← Category.assoc, prod.comp_lift, 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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw :
  f ≫
      CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift g h : Y ⟶ Limits.prod.{v, u} Z Z)
        (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (f ≫ prod.lift g h : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ g) (f ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ g - f ≫ h
⊢ f ≫ (g - h) = f ≫ g - f ≫ h
have rw₃ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ g) (f ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ g) (f ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z)
Tactic: rw [sub_def, ← Category.assoc, prod.comp_lift, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
    h =
  f ≫ h - g ≫ h
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
      h =
    f ≫ h - g ≫ h
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw₁ : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
    (σ ≫ h : Limits.prod.{v, u} Y Y ⟶ Z) =
  f ≫ h - g ≫ h
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
      h =
    f ≫ h - g ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
      (σ ≫ h : Limits.prod.{v, u} Y Y ⟶ Z) =
    f ≫ h - g ≫ h
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw₂ : CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.map h h : Limits.prod.{v, u} Y Y ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z)) =
  f ≫ h - g ≫ h
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
      h =
    f ≫ h - g ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
      (σ ≫ h : Limits.prod.{v, u} Y Y ⟶ Z) =
    f ≫ h - g ≫ h
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
        (prod.map h h : Limits.prod.{v, u} Y Y ⟶ Limits.prod.{v, u} Z Z) (σ : Limits.prod.{v, u} Z Z ⟶ Z)) =
    f ≫ h - g ≫ h
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw₃ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g) (prod.map h h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  f ≫ h - g ≫ h
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
      h =
    f ≫ h - g ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
      (σ ≫ h : Limits.prod.{v, u} Y Y ⟶ Z) =
    f ≫ h - g ≫ h
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
        (prod.map h h : Limits.prod.{v, u} Y Y ⟶ Limits.prod.{v, u} Z Z) (σ : Limits.prod.{v, u} Z Z ⟶ Z)) =
    f ≫ h - g ≫ h
rw₃ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g) (prod.map h h) : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ h - g ≫ h
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw₄ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ h) (g ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  f ≫ h - g ≫ h
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y) ≫
      h =
    f ≫ h - g ≫ h
rw₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g : X ⟶ Limits.prod.{v, u} Y Y)
      (σ ≫ h : Limits.prod.{v, u} Y Y ⟶ Z) =
    f ≫ h - g ≫ h
rw₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
        (prod.map h h : Limits.prod.{v, u} Y Y ⟶ Limits.prod.{v, u} Z Z) (σ : Limits.prod.{v, u} Z Z ⟶ Z)) =
    f ≫ h - g ≫ h
rw₃ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift f g) (prod.map h h) : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ h - g ≫ h
rw₄ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ h) (g ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
      (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
    f ≫ h - g ≫ h
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
have rw₅ : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ h) (g ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z) =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (f ≫ h) (g ≫ h) : X ⟶ Limits.prod.{v, u} Z Z)
    (σ : Limits.prod.{v, u} Z Z ⟶ Z)
Tactic: rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, 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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw : f ≫ (g - -h) = f ≫ g + f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₂ : f ≫ g - f ≫ (0 - h) = f ≫ g + f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
rw₂ : f ≫ g - f ≫ (0 - h) = f ≫ g + f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₃ : f ≫ g - (f ≫ 0 - f ≫ h) = f ≫ g + f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
rw₂ : f ≫ g - f ≫ (0 - h) = f ≫ g + f ≫ h
rw₃ : f ≫ g - (f ≫ 0 - f ≫ h) = f ≫ g + f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₄ : f ≫ g - (0 - f ≫ h) = f ≫ g + f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
rw₂ : f ≫ g - f ≫ (0 - h) = f ≫ g + f ≫ h
rw₃ : f ≫ g - (f ≫ 0 - f ≫ h) = f ≫ g + f ≫ h
rw₄ : f ≫ g - (0 - f ≫ h) = f ≫ g + f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₅ : f ≫ g - (0 - f ≫ h) = f ≫ g - -f ≫ h
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f : X ⟶ Y
g h : Y ⟶ Z
rw : f ≫ (g - -h) = f ≫ g + f ≫ h
rw₁ : f ≫ g - f ≫ (-h) = f ≫ g + f ≫ h
rw₂ : f ≫ g - f ≫ (0 - h) = f ≫ g + f ≫ h
rw₃ : f ≫ g - (f ≫ 0 - f ≫ h) = f ≫ g + f ≫ h
rw₄ : f ≫ g - (0 - f ≫ h) = f ≫ g + f ≫ h
rw₅ : f ≫ g - (0 - f ≫ h) = f ≫ g - -f ≫ h
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have rw₆ : f ≫ g - (0 - f ≫ h) = f ≫ g - (0 - f ≫ h)
Tactic: rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw : (f - -g) ≫ h = f ≫ h + g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₂ : f ≫ h - (0 - g) ≫ h = f ≫ h + g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
rw₂ : f ≫ h - (0 - g) ≫ h = f ≫ h + g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₃ : f ≫ h - (0 ≫ h - g ≫ h) = f ≫ h + g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
rw₂ : f ≫ h - (0 - g) ≫ h = f ≫ h + g ≫ h
rw₃ : f ≫ h - (0 ≫ h - g ≫ h) = f ≫ h + g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₄ : f ≫ h - (0 - g ≫ h) = f ≫ h + g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
rw₂ : f ≫ h - (0 - g) ≫ h = f ≫ h + g ≫ h
rw₃ : f ≫ h - (0 ≫ h - g ≫ h) = f ≫ h + g ≫ h
rw₄ : f ≫ h - (0 - g ≫ h) = f ≫ h + g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₅ : f ≫ h - (0 - g ≫ h) = f ≫ h - -g ≫ h
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
rw : (f - -g) ≫ h = f ≫ h + g ≫ h
rw₁ : f ≫ h - (-g) ≫ h = f ≫ h + g ≫ h
rw₂ : f ≫ h - (0 - g) ≫ h = f ≫ h + g ≫ h
rw₃ : f ≫ h - (0 ≫ h - g ≫ h) = f ≫ h + g ≫ h
rw₄ : f ≫ h - (0 - g ≫ h) = f ≫ h + g ≫ h
rw₅ : f ≫ h - (0 - g ≫ h) = f ≫ h - -g ≫ h
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have rw₆ : f ≫ h - (0 - g ≫ h) = f ≫ h - (0 - g ≫ h)
Tactic: rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq (α := X ⟶ Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
    (f ≫ Quiver.Hom.unop (kernel.ι f.op)) 0
have rw : Eq.{v_1 + 1} (α := X ⟶ Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
  (Quiver.Hom.unop (kernel.ι f.op ≫ f.op)) 0
Tactic: rw [← f.unop_op, ← unop_comp, f.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
      (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
    (CategoryStruct.comp (Y := cokernel f)
      (Quiver.Hom.unop (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯) :
        Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op) ⟶
          Opposite.unop (Opposite.op (cokernel f)))
      (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) ⋯))
    (𝟙 (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
have rw : Eq.{v_1 + 1} (α :=
  Quiver.Hom.{v_1, u_1} (V := C) (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op))
    (Opposite.unop (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y := Opposite.op (cokernel f))
      (Quiver.Hom.op (cokernel.desc f (Quiver.Hom.unop (kernel.ι f.op)) sorry))
      (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) sorry)))
  (Quiver.Hom.unop (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
Tactic: rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]