C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a + b = b + a
rw [add_def]
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ - -a - -b = b + a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a
conv_lhs => rw [← neg_neg a]
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ - -a - -b = b + a
rw [neg_def, neg_def, neg_def, sub_sub_sub]
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (-b - a) = b + a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a
conv_lhs =>
  congr
  next => skip
  rw [← neg_def, neg_sub]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (-b - a) = b + a
rw [sub_sub_sub, add_def, ← neg_def, neg_neg b, neg_def]