no goals
C : Type u
A : Type ?u.194994
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorAdd' C n m 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    (shiftFunctorAdd' C m n 0 (_ : m + n = 0)).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).hom.app X) =
    (shiftFunctorCompIsoId C m n (_ : m + n = 0)).hom.app ((shiftFunctor C n).obj X)
dsimp [shiftFunctorCompIsoId]
no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorAdd' C n m 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    (shiftFunctorAdd' C m n 0 (_ : m + n = 0)).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)
simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X,
  ← shiftFunctorAdd'_add_zero_inv_app n X]
  using shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h
    (by rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]) (by rw [h, zero_add]) X
no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]
no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ n + m + n = n
rw [h, zero_add]