C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - -b + c = a + (b + c)
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + b + c = a + (b + c)
conv_lhs =>
  congr; rw [add_def]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - -b + c = a + (b + c)
rw [sub_add, ← add_neg, neg_sub', neg_neg]