awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ 𝟙 (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
have 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))
Tactic: rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
⊢ (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))
have 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) sorry))
      (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 sorry)) (Opposite.unop 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
⊢ 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)))
have 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) sorry))
        (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 sorry)) (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: 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⟧' = 𝟙 _
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X : Cᵒᵖ
⊢ 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)))
have 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) sorry))
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (Opposite.unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) sorry))
      (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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)))
⊢ 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)))
have 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))))
Tactic: rw [shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app n X.unop, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ 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))))
have 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 sorry)) (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: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ 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)))
have 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 sorry)) (Opposite.unop X)))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n m hnm)) (Opposite.unop X)))
have obtain : ∀ (hnm : n + -n = 0),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ 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.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n m hnm)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C n m hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))))
have 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.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n)) X)
    (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) hnm)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) hnm))
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X))))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ 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 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X)
    (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X))))
have a : Eq.{v_1 + 1} (α :=
  Opposite.unop
      (Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X) ⟶
    Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))
  (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
  (Quiver.Hom.unop
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0))
          X) ⟶
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
    (Quiver.Hom.unop
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op
          (Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)))))
have a : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
    Opposite.unop X)
  (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 sorry)) (Opposite.unop X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
  (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
Tactic: dsimp [opShiftFunctorEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
        Opposite.unop X)
have a : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
    Opposite.unop X)
  (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 sorry)) (Opposite.unop X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
  (Functor.map (shiftFunctor C (A := ℤ) 0)
        (Quiver.Hom.unop
          (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)) ⟶
      Opposite.unop X)
Tactic: rw [shiftFunctorZero_op_inv_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_hom_app, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X)
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))
have a : Eq.{v_1 + 1} (α :=
  Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X) ⟶
    Opposite.unop
      (Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 0) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 0)) X))
  (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 0))) X))
  (Quiver.Hom.unop
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))))
Tactic: apply Quiver.Hom.unop_inj