awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
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
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.snd =
    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.snd
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
rw :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
          (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a b : 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 c d : X ⟶ Limits.prod.{v, u} Y Y)
            (σ : Limits.prod.{v, u} Y Y ⟶ Y)) :
        X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a - b - (c - d)
⊢ a - c - (b - d) = a - b - (c - d)

Tactic:
rw [sub_def, ← lift_sub_lift, sub_def, Category.assoc, σ_comp, prod.lift_map_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NonPreadditiveAbelian.σ_comp, CategoryTheory.Limits.prod.lift_map_assoc, CategoryTheory.NonPreadditiveAbelian.lift_sub_lift, CategoryTheory.NonPreadditiveAbelian.sub_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
          (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a b : 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 c d : X ⟶ Limits.prod.{v, u} Y Y)
            (σ : Limits.prod.{v, u} Y Y ⟶ Y)) :
        X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    a - b - (c - d)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : -b - a
| -a - b

Tactic:
rw [neg_def, ← sub_zero b, sub_sub_sub, sub_zero, ← neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.sub_zero, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
conv_lhs : -a - b = -b - a
conv_lhs₁ : -b - a = -b - a
⊢ -a - b = -b - a

Tactic:
conv_lhs => rw [neg_def, ← sub_zero b, sub_sub_sub, sub_zero, ← neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.sub_zero, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw : 0 - (0 - a) = a
⊢ - -a = a

Tactic:
rw [neg_def, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : 0
a₂ : 0 - a
| 0 - (0 - a)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a - a
| 0

Tactic:
rw [← sub_self a]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
a₁ : a - a
a₂ : 0 - a
| 0 - (0 - a)

Tactic:
congr; rw [← sub_self a]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
conv_lhs : a - a - (0 - a) = a
⊢ 0 - (0 - a) = a

Tactic:
conv_lhs =>
    congr; rw [← sub_self a]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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) = a
rw₁ : a - (a - a) = a
rw₂ : a - 0 = a
rw₃ rw₄ : a = a
⊢ a - a - (0 - a) = a

Tactic:
rw [sub_sub_sub, sub_zero, sub_self, sub_zero]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.sub_zero, CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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 = b + a
⊢ a + b = b + a

Tactic:
rw [add_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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

Tactic:
rw [← neg_neg a]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
conv_lhs : - -a - -b = b + a
⊢ a - -b = b + a

Tactic:
conv_lhs => rw [← neg_neg a]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : HSub.hSub (α := X ⟶ Y) 0 0 - (0 - a - b) = b + a
⊢ - -a - -b = b + a

Tactic:
rw [neg_def, neg_def, neg_def, sub_sub_sub]

Premises used: CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
congr : HSub.hSub (α := X ⟶ Y) 0 0
a₁ : 0 - a - b
| HSub.hSub (α := X ⟶ Y) 0 0 - (0 - a - b)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
| HSub.hSub (α := X ⟶ Y) 0 0

Tactic:
next => skip
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
a₁ : -b - a
| 0 - a - b

Tactic:
rw [← neg_def, neg_sub]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
a₁ : -b - a
| HSub.hSub (α := X ⟶ Y) 0 0 - (0 - a - b)

Tactic:
congr
    next => skip
    rw [← neg_def, neg_sub]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
conv_lhs : HSub.hSub (α := X ⟶ Y) 0 0 - (-b - a) = b + a
⊢ HSub.hSub (α := X ⟶ Y) 0 0 - (0 - a - b) = b + a

Tactic:
conv_lhs =>
    congr
    next => skip
    rw [← neg_def, neg_sub]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : 0 - -b - (0 - a) = b + a
rw₁ : 0 - -b - (0 - a) = b - -a
rw₂ : - -b - (0 - a) = b - -a
rw₃ : b - (0 - a) = b - -a
rw₄ rw₅ : b - (0 - a) = b - (0 - a)
⊢ HSub.hSub (α := X ⟶ Y) 0 0 - (-b - a) = b + a

Tactic:
rw [sub_sub_sub, add_def, ← neg_def, neg_neg b, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.neg_def, CategoryTheory.NonPreadditiveAbelian.neg_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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₁ rw₂ : a - b = a - b
⊢ a + -b = a - b

Tactic:
rw [add_def, neg_neg]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.neg_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw : a - a = 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ a + -a = 0

Tactic:
rw [add_neg, sub_self]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_neg, CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a : X ⟶ Y
rw : a + -a = 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ -a + a = 0

Tactic:
rw [add_comm, add_neg_cancel]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_comm, CategoryTheory.NonPreadditiveAbelian.add_neg_cancel
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : 0 - (a - b) = 0 - a + b
⊢ -(a - b) = -a + b

Tactic:
rw [neg_def, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : HSub.hSub (α := X ⟶ Y) 0 0 - (a - b)
| 0 - (a - b)

Tactic:
rw [← sub_self (0 : X ⟶ Y)]

Premises used: OfNat.ofNat, CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
conv_lhs : HSub.hSub (α := X ⟶ Y) 0 0 - (a - b) = 0 - a + b
⊢ 0 - (a - b) = 0 - a + b

Tactic:
conv_lhs => rw [← sub_self (0 : X ⟶ Y)]

Premises used: OfNat.ofNat, CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b : X ⟶ Y
rw : 0 - a - (0 - b) = 0 - a + b
rw₁ : 0 - a - (0 - b) = 0 - a - -b
rw₂ rw₃ : 0 - a - (0 - b) = 0 - a - (0 - b)
⊢ HSub.hSub (α := X ⟶ Y) 0 0 - (a - b) = 0 - a + b

Tactic:
rw [sub_sub_sub, add_def, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₂ rw₃ : -a - b = -a - b
⊢ -(a + b) = -a - b

Tactic:
rw [add_def, neg_sub', add_neg]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_sub', CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.add_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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)
rw₃ rw₄ : a - (b - c) = a - (b - c)
⊢ a - b + c = a - (b - c)

Tactic:
rw [add_def, neg_def, sub_sub_sub, sub_zero]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.sub_sub_sub, CategoryTheory.NonPreadditiveAbelian.sub_zero, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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₂ : c
| a + b + c

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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

Tactic:
rw [add_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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₂ : c
| a + b + c

Tactic:
congr; rw [add_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c : X ⟶ Y
conv_lhs : a - -b + c = a + (b + c)
⊢ a + b + c = a + (b + c)

Tactic:
conv_lhs =>
    congr; rw [add_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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)
rw₃ rw₄ : a + (b + c) = a + (b + c)
⊢ a - -b + c = a + (b + c)

Tactic:
rw [sub_add, ← add_neg, neg_sub', neg_neg]

Premises used: CategoryTheory.NonPreadditiveAbelian.neg_sub', CategoryTheory.NonPreadditiveAbelian.sub_add, CategoryTheory.NonPreadditiveAbelian.add_neg, CategoryTheory.NonPreadditiveAbelian.neg_neg
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₃ rw₄ : a = a
⊢ a + 0 = a

Tactic:
rw [add_def, neg_def, sub_self, sub_zero]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.sub_zero, CategoryTheory.NonPreadditiveAbelian.neg_def, CategoryTheory.NonPreadditiveAbelian.sub_self
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₃ 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)
⊢ f ≫ (g - h) = f ≫ g - f ≫ h

Tactic:
rw [sub_def, ← Category.assoc, prod.comp_lift, sub_def]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.comp_lift, CategoryTheory.NonPreadditiveAbelian.sub_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₅ 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)
⊢ (f - g) ≫ h = f ≫ h - g ≫ h

Tactic:
rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, sub_def]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_map, CategoryTheory.NonPreadditiveAbelian.σ_comp, CategoryTheory.NonPreadditiveAbelian.sub_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₆ rw₇ : f ≫ g - (0 - f ≫ h) = f ≫ g - (0 - f ≫ h)
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.Limits.comp_zero, CategoryTheory.NonPreadditiveAbelian.comp_sub, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
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
rw₆ rw₇ : f ≫ h - (0 - g ≫ h) = f ≫ h - (0 - g ≫ h)
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_def]

Premises used: CategoryTheory.NonPreadditiveAbelian.add_def, CategoryTheory.NonPreadditiveAbelian.sub_comp, CategoryTheory.Limits.zero_comp, CategoryTheory.NonPreadditiveAbelian.neg_def
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α := Opposite.op (cokernel f) ⟶ Opposite.op X) (Quiver.Hom.op (cokernel.π f) ≫ f.op) 0

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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
⊢ 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

Tactic:
rw [← f.unop_op, ← unop_comp, f.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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} (α := 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:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Opposite
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
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)) ⋯))
        (kernel.lift f.op (Quiver.Hom.op (cokernel.π f)) ⋯)))
    (Quiver.Hom.unop (𝟙 (kernel.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)))
⊢ 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)))

Tactic:
rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]

Premises used: CategoryTheory.Limits.cokernel.desc, Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.unop_id