awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
erw :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (NatTrans.app
        (Iso.hom
          (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
            (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ ⋯))
        X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, 0} C ℤ) b₁ b₂ b₃ ⋯)) X ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (Functor.map
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (NatTrans.app
              (Iso.inv
                (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ ⋯))
              X)))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))

Tactic:
erw [@pullbackShiftFunctorAdd'_hom_app (OppositeShift C ℤ) _ _ _ _ _ _ _ X
    a₁ a₂ a₃ h b₁ b₂ b₃ (by dsimp; lia) (by dsimp; lia) (by dsimp; lia)]

Premises used: CategoryTheory.pullbackShiftFunctorAdd'_hom_app
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₃) X)
      (NatTrans.app
        (Iso.hom
          (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
            (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ ⋯))
        X)
      (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (Functor.map
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (NatTrans.app
              (Iso.inv
                (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ ⋯))
              X))))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X)) ≫
            NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
                (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
              Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h)) X)
    (Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₁ b₁ h₁)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X)

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,
    assoc, assoc, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, Opposite, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app, CategoryTheory.shiftFunctorAdd', CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
erw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X)) ≫
            NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
                (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
              Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X

Tactic:
erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₃ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫ NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₄ rw₅ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X)
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X))
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X

Tactic:
rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.op_comp_assoc, CategoryTheory.Category.id_comp, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
K L : Cᵒᵖ
φ : K ⟶ L
n m : ℤ
hnm : n + m = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) K ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) L)
    (Functor.map (shiftFunctor Cᵒᵖ n) φ)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m hnm)) K ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C m) φ.unop) ≫ NatTrans.app (Iso.inv (shiftFunctorOpIso C n m hnm)) L)

Tactic:
(NatIso.naturality_2 (shiftFunctorOpIso C n m hnm) φ).symm

Premises used: Quiver.Hom.op, CategoryTheory.NatIso.naturality_2, CategoryTheory.Pretriangulated.shiftFunctorOpIso, Eq.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
erw :
  Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
          (Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (Quiver.Hom.unop
        (Functor.map (shiftFunctor Cᵒᵖ n)
          (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X))))))
    (𝟙 (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
⊢ (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)) ≫
        𝟙
          (Opposite.unop
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))) ≫
      Quiver.Hom.unop
        (Functor.map (shiftFunctor Cᵒᵖ n)
          (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) ≫
            Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))))) =
    𝟙 (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))

Tactic:
erw [comp_id, Functor.map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
change :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Opposite.unop X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ≫
        Functor.map (shiftFunctor C (-n))
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Opposite.unop X)))
    (𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
          (Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (Quiver.Hom.unop
        (Functor.map (shiftFunctor Cᵒᵖ n)
          (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X))))))
    (𝟙 (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))

Tactic:
change (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X.unop⟦-n⟧) ≫
      ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X.unop)⟦-n⟧' = 𝟙 _

Premises used: add_neg_cancel, CategoryTheory.shiftFunctor, CategoryTheory.CategoryStruct.id, neg_add_cancel, CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.Iso.hom, Opposite.unop, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
rw :
  CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ shiftFunctor C (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))
      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))) =
    𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))
rw₁ rw₂ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Opposite.unop X)))
    (𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
    (𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Opposite.unop X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ≫
        Functor.map (shiftFunctor C (-n))
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Opposite.unop X)))
    (𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X))) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))

Tactic:
rw [shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app n X.unop, Iso.inv_hom_id_app]

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app, CategoryTheory.Iso.inv_hom_id_app, Opposite.unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X)
      (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) hnm)) X))))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m hnm)) X))))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) hnm)) X))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) opShiftFunctorEquivalence_unitIso_inv_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
          X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
      (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) hnm)) X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-n) n ⋯)) (Opposite.unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m hnm)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m n ⋯)) (Opposite.unop X)))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl