awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
B : C
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    T
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
obtain :
  ∀ (x₃ : (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₃ ⟶ B)
    (hx₃ : x₂ = (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₂ ≫ x₃),
    ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
              AddCommGrpCat.carrier) (X :=
              ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B)))
              (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) :
            (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₁ : Type v_1)) →
              (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂ : Type v_1))
          x₁ =
        x₂
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
            AddCommGrpCat.carrier) (X :=
            ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂ : Type v_1))
        x₁ =
      x₂

Tactic:
obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, CategoryTheory.Pretriangulated.unop_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
B : C
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    T
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
x₃ : (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₃ ⟶ B
hx₃ : x₂ = (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₂ ≫ x₃
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
            AddCommGrpCat.carrier) (X :=
            ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂ : Type v_1))
        x₁ =
      x₂

Tactic:
⟨x₃, hx₃.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
B : C
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    T
x₂ : unop T.obj₂ ⟶ B
hx₂ : T.mor₂.unop ≫ x₂ = 0
x₃ : (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₃ ⟶ B
hx₃ : x₂ = (unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₂ ≫ x₃
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
            AddCommGrpCat.carrier) (X :=
            ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂ : Type v_1))
        x₁ =
      x₂

Tactic:
exact ⟨x₃, hx₃.symm⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_1 inst_4 _) T
B : C
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).op.map (Functor.obj preadditiveYoneda B))

Tactic:
(preadditiveYoneda.obj B).map_distinguished_op_exact T hT

Premises used: CategoryTheory.preadditiveYoneda, CategoryTheory.Functor.map_distinguished_op_exact, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) T.obj₃
⊢ 1 + n₀ = n₁

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) T.obj₃
⊢ Eq (α := (↑(Functor.obj (Functor.shift (Functor.obj preadditiveCoyoneda A) n₁) T.obj₁) : Type v_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
            AddCommGrpCat.carrier) (X := Functor.obj (Functor.shift (Functor.obj preadditiveCoyoneda A) n₀) T.obj₃)
            (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda A) T n₀ n₁ h) :
          (a : (↑(((preadditiveCoyoneda.obj A).shift n₀).obj T.obj₃) : Type v_1)) →
            (↑(((preadditiveCoyoneda.obj A).shift n₁).obj T.obj₁) : Type v_1))
        x :
      (↑(Functor.obj (Functor.shift (Functor.obj preadditiveCoyoneda A) n₁) T.obj₁) : Type v_1))
    (x ≫ Functor.map (shiftFunctor C n₀) T.mor₃ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C 1 n₀ n₁ ⋯)) T.obj₁ :
      unop A ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₁) T.obj₁)

Tactic:
apply Category.assoc

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
B : C
a : ℤ
x : Cᵒᵖ
x_1 :
  (↑(Functor.obj
        (shiftFunctor Cᵒᵖ (A := ℤ) 0 ⋙
          Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
        x) :
    Type v_1)
⊢ Eq (α :=
    (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) x) :
      Type v_1))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (A : Cᵒᵖ) ↦
                    AddEquiv.toAddCommGrpIso
                      (let __Equiv :
                        (↑(Functor.obj
                                (shiftFunctor Cᵒᵖ (A := ℤ) 0 ⋙
                                  Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                                A) :
                            Type v_1) ≃
                          (↑(Functor.obj
                                (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                                A) :
                            Type v_1) :=
                        Equiv.trans Quiver.Hom.opEquiv (Equiv.symm (ShiftedHom.opEquiv' 0 a a ⋯));
                      { toEquiv := __Equiv, map_add' := ⋯ }))
                  ⋯))
              x) :
          (a_1 : (↑((shiftFunctor Cᵒᵖ 0 ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x) : Type v_1)) →
            (↑((preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x) : Type v_1))
        x_1 :
      (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) x) :
        Type v_1))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (Iso.hom
                (Functor.isoWhiskerRight (shiftFunctorZero Cᵒᵖ ℤ)
                    (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) ≪≫
                  Functor.leftUnitor
                    (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))))
              x) :
          (a_1 : (↑((shiftFunctor Cᵒᵖ 0 ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x) : Type v_1)) →
            (↑((preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x) : Type v_1))
        x_1 :
      (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) x) :
        Type v_1))

Tactic:
apply ShiftedHom.opEquiv'_zero_add_symm

Premises used: CategoryTheory.ShiftedHom.opEquiv'_zero_add_symm
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B
⊢ a + n = a'

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B
symm :
  Eq (α := (↑(Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a') Y) : Type v_1))
    (ShiftedHom.comp (a := n)
      ((Equiv.symm (ShiftedHom.opEquiv n) :
          (a : ShiftedHom (op (unop X)) (op (unop Y)) n) → ShiftedHom (unop Y) (unop X) n)
        f)
      z ⋯)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
          AddCommGrpCat.carrier) (X := Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a) X)
          (Functor.shiftMap (Functor.obj preadditiveYoneda B) f a a' h) :
        (a : (↑(((preadditiveYoneda.obj B).shift a).obj X) : Type v_1)) →
          (↑(((preadditiveYoneda.obj B).shift a').obj Y) : Type v_1))
      z)
⊢ Eq (α := (↑(Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a') Y) : Type v_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
            AddCommGrpCat.carrier) (X := Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a) X)
            (Functor.shiftMap (Functor.obj preadditiveYoneda B) f a a' h) :
          (a : (↑(((preadditiveYoneda.obj B).shift a).obj X) : Type v_1)) →
            (↑(((preadditiveYoneda.obj B).shift a').obj Y) : Type v_1))
        z :
      (↑(Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a') Y) : Type v_1))
    (ShiftedHom.comp (a := n)
        ((Equiv.symm (ShiftedHom.opEquiv n) :
            (a : ShiftedHom (op (unop X)) (op (unop Y)) n) → ShiftedHom (unop Y) (unop X) n)
          f)
        z ⋯ :
      ShiftedHom (unop Y) B a')

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B
⊢ Eq (α := (↑(Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a') Y) : Type v_1))
    (ShiftedHom.comp (a := n)
      ((Equiv.symm (ShiftedHom.opEquiv n) :
          (a : ShiftedHom (op (unop X)) (op (unop Y)) n) → ShiftedHom (unop Y) (unop X) n)
        f)
      z ⋯)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
          AddCommGrpCat.carrier) (X := Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) a) X)
          (Functor.shiftMap (Functor.obj preadditiveYoneda B) f a a' h) :
        (a : (↑(((preadditiveYoneda.obj B).shift a).obj X) : Type v_1)) →
          (↑(((preadditiveYoneda.obj B).shift a').obj Y) : Type v_1))
      z)

Tactic:
apply ShiftedHom.opEquiv_symm_apply_comp

Premises used: CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
simp :
  CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B))
      ((Equiv.symm (ShiftedHom.opEquiv 1) :
            (a :
                ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
                  (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
          (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) x)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n₀ 1 n₁ ⋯)) B) =
    (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) x) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C n₀ 1 n₁ h)) B
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v_1}) ↦ (↑x1 : Type v_1) →+ (↑x2 : Type v_1)) (CC :=
          AddCommGrpCat.carrier) (X :=
          Functor.obj (Functor.shift (Functor.obj preadditiveYoneda B) n₀)
            (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃)
          (Functor.homologySequenceδ (Functor.obj preadditiveYoneda B)
            (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)) n₀ n₁ h) :
        (a :
            (↑(((preadditiveYoneda.obj B).shift n₀).obj ((triangleOpEquivalence C).functor.obj (op T)).obj₃) :
              Type v_1)) →
          (↑(((preadditiveYoneda.obj B).shift n₁).obj ((triangleOpEquivalence C).functor.obj (op T)).obj₁) : Type v_1))
      x =
    T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) x ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C n₀ 1 n₁ h)) B

Tactic:
simp only [Functor.homologySequenceδ, preadditiveYoneda_shiftMap_apply,
    ShiftedHom.comp, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShiftedHom.comp, CategoryTheory.Functor.homologySequenceδ, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
e_a :
  (Equiv.symm (ShiftedHom.opEquiv 1) :
        (a :
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
          ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
            (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
      (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ =
    T.mor₃
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B))
      ((Equiv.symm (ShiftedHom.opEquiv 1) :
            (a :
                ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
                  (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
          (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) x)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n₀ 1 n₁ ⋯)) B) =
    (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) x) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C n₀ 1 n₁ h)) B

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
e_a :
  Eq (α :=
    ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
      (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        ((Equiv.symm (ShiftedHom.opEquiv 1) :
              (a :
                  ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
                    (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
                ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                  (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
            (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ :
          ShiftedHom (M := ℤ) (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)
            (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃) 1) :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        T.mor₃ :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
⊢ (Equiv.symm (ShiftedHom.opEquiv 1) :
        (a :
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
          ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
            (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
      (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ =
    T.mor₃

Tactic:
apply (ShiftedHom.opEquiv _).injective

Premises used: Equiv.injective, CategoryTheory.ShiftedHom.opEquiv