awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
rw₂ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ f.map G)
rw₃ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₄ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₅ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (F.map f ≫
      τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₆ rw₇ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫
      τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
    (F.map f ≫
      τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)

Tactic:
rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShiftedHom.comp_mk₀, CategoryTheory.ShiftedHom.mk₀_comp, CategoryTheory.ShiftedHom.map, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift e.hom M
⊢ Eq (α := ShiftedHom (G.obj X) (G.obj Y) a) (comp (mk₀ 0 ⋯ (e.inv.app X)) (comp (f.map F) (mk₀ 0 ⋯ (e.hom.app Y)) ⋯) ⋯)
    (f.map G)

Tactic:
simp [map_naturality]

Premises used: CategoryTheory.ShiftedHom.map_naturality
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift e.hom M
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Y) a) (comp (mk₀ 0 ⋯ (e.hom.app X)) (comp (f.map G) (mk₀ 0 ⋯ (e.inv.app Y)) ⋯) ⋯)
    (f.map F)

Tactic:
map_naturality_1 f e.symm

Premises used: CategoryTheory.ShiftedHom.map_naturality_1, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
dsimp :
  Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
    (F.map (f ≫ Functor.map (shiftFunctor C a) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
    (CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj Y))
      (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y)
      (Functor.map (shiftFunctor D a) (F.map g ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Z) c) ((f.comp g h).map F) (comp (f.map F) (g.map F) h)

Tactic:
dsimp [comp, map]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.ShiftedHom.map
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
simp :
  Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
    (F.map f ≫
      F.map (Functor.map (shiftFunctor C a) g) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
    (F.map f ≫
      F.map (Functor.map (shiftFunctor C a) g) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z)))
          (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
    (F.map (f ≫ Functor.map (shiftFunctor C a) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
    (CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj Y))
      (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y)
      (Functor.map (shiftFunctor D a) (F.map g ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))

Tactic:
simp only [Functor.map_comp, assoc, ← Functor.commShiftIso_hom_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_hom_naturality_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
    (F.map f ≫
      F.map (Functor.map (shiftFunctor C a) g) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
    (F.map f ≫
      F.map (Functor.map (shiftFunctor C a) g) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z)))
          (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))

Tactic:
simp only [F.commShiftIso_add' h, Functor.CommShift.isoAdd'_hom_app,
    ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.comp_obj, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.commShiftIso_add', CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.CommShift.isoAdd'_hom_app, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
a : M
α₁ α₂ : ShiftedHom X Y a
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : F.CommShift M
inst_8 : F.Additive
⊢ (α₁ + α₂).map F = HAdd.hAdd (α := ShiftedHom (F.obj X) (F.obj Y) a) (α₁.map F) (α₂.map F)

Tactic:
simp [ShiftedHom.map, F.map_add]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.ShiftedHom.map
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
a : M
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : F.CommShift M
inst_8 : F.Additive
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Y) a) (map 0 F) 0

Tactic:
simp [ShiftedHom.map]

Premises used: CategoryTheory.ShiftedHom.map
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
rw₁ :
  α ≫
      HSMul.hSMul (β :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α.comp β h
rw₂ :
  α ≫
      HSMul.hSMul (β :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₃ :
  α ≫ (r • Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₄ rw₅ :
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]

Premises used: CategoryTheory.Functor.map_smul, CategoryTheory.ShiftedHom.comp, CategoryTheory.Linear.comp_smul, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : (r • α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
rw₁ :
  (r • α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₂ rw₃ :
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
rw [comp, comp, Linear.smul_comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y : C
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
m₀ : M
hm₀ : m₀ = 0
r : R
f : X ⟶ Y
⊢ mk₀ m₀ hm₀ (r • f) = HSMul.hSMul (β := ShiftedHom X Y m₀) r (mk₀ m₀ hm₀ f)

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
R : Type u_5
inst_5 : Ring R
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Linear.{u_5, v_1, u_1} R C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : Linear.{u_5, v_2, u_2} R D
r : R
a : M
α : ShiftedHom X Y a
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_10 : F.CommShift M
inst_11 : Functor.Linear R F
⊢ (r • α).map F = HSMul.hSMul (β := ShiftedHom (F.obj X) (F.obj Y) a) r (α.map F)

Tactic:
simp [ShiftedHom.map, F.map_smul]

Premises used: CategoryTheory.Functor.map_smul, CategoryTheory.ShiftedHom.map
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n : ℤ
f : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ Eq (α := ShiftedHom X Y n)
    ((Equiv.symm (opEquiv n) : (a : ShiftedHom (Opposite.op Y) (Opposite.op X) n) → ShiftedHom X Y n) f :
      ShiftedHom X Y n)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            (Opposite.op X)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)))
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop f)) :
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop (Opposite.op Y)))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
rw :
  Eq (α := ShiftedHom Y Z c)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
            (Opposite.op Y)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f)) ≫
      Functor.map (shiftFunctor C a) z ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
            (Opposite.op Y)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop (Quiver.Hom.op z ≫ f))) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
⊢ Eq (α := ShiftedHom Y Z c)
    (comp ((Equiv.symm (opEquiv a) : (a_1 : ShiftedHom (Opposite.op X) (Opposite.op Y) a) → ShiftedHom Y X a) f) z h)
    ((Equiv.symm (opEquiv a) :
          (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C b).obj Z)) (Opposite.op Y) a) →
            ShiftedHom Y ((shiftFunctor C b).obj Z) a)
        (Quiver.Hom.op z ≫ f) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)

Tactic:
rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply,
    ShiftedHom.comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.ShiftedHom.opEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ Eq (α := ShiftedHom Y Z c)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)) :
          Opposite.unop (Opposite.op Y) ⟶
            Opposite.unop
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      Functor.map (shiftFunctor C a) z ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)) :
          Opposite.unop (Opposite.op Y) ⟶
            Opposite.unop
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))))))
        (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f ≫ z) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op Y))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)

Tactic:
simp only [assoc, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ a + b = c

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n a a' : ℤ
h : n + a = a'
⊢ a + n = a'

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n a : ℤ
f :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ a + n = a'

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n a : ℤ
f :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ Eq (α := ShiftedHom X Y a')
    ((Equiv.symm (opEquiv' n a a' h) :
          (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
        f :
      ShiftedHom X Y a')
    ((Equiv.symm (opEquiv n) :
            (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
              ShiftedHom X ((shiftFunctor C a).obj Y) n)
          f ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
a' : ℤ
f : ShiftedHom X Y a'
n a : ℤ
h : n + a = a'
⊢ a + n = a'

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a' : ℤ
f : ShiftedHom X Y a'
n a : ℤ
h : n + a = a'
⊢ Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X))
    ((opEquiv' n a a' h :
          (a_1 : ShiftedHom X Y a') → Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
        f :
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X))
    ((opEquiv n :
          (a_1 : ShiftedHom X ((shiftFunctor C a).obj Y) n) →
            ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n)
        (f ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C a n a' ⋯)) Y) :
      ShiftedHom (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)) (Opposite.op X) n)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ m + n = q

Tactic:
lia