-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
/--
If `f : X ⟶ Y⟦m⟧`, `n + m = 0` and `ha' : m + a = a'`, this lemma relates the two
morphisms `F.shiftMap f a a' ha'` and `(F.shift a').map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identify to morphisms
`(F.shift a).obj X ⟶ (F.shift a').obj Y`.
-/
lemma shiftIso_hom_app_comp_shiftMap_of_add_eq_zero [F.ShiftSequence G]
    {X Y : C} {m : G} (f : X ⟶ Y⟦m⟧)
    (n : G) (hnm : n + m = 0) (a a' : G) (ha' : m + a = a') :
    (F.shiftIso n a' a (by rw [← ha', ← add_assoc, hnm, zero_add])).hom.app X ≫
      F.shiftMap f a a' ha' =
    (F.shift a').map (f⟦n⟧' ≫ (shiftFunctorCompIsoId C m n
      (by rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero])).hom.app Y)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + n = 0

Tactic:
rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁷ : Category.{?u.86177, u_1} C
inst✝⁶ : Category.{?u.86181, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
G : Type u_4
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + n = 0

Tactic:
rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ (F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)

Tactic:
have hnm' : m + n = 0 := by
  rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]

Result:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
hnm' : m + n = 0
⊢ (F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁷ : Category.{?u.86177, u_1} C
inst✝⁶ : Category.{?u.86181, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
G : Type u_4
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ n + a' = a

Tactic:
rw [← ha', ← add_assoc, hnm, zero_add]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
hnm' : m + n = 0
⊢ (F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)

Tactic:
simp [F.shiftIso_hom_app_comp_shiftMap f n 0 hnm' a' a, shiftIso_zero_hom_app,
  shiftFunctorCompIsoId]

Result:
no goals