awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_4 :
  NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
      (Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂ =
    v₁₃ ≫ u₁₂
⊢ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂ =
    v₁₃ ≫ u₁₂

Tactic:
nth_rw 2 [← assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_5 :
  Triangle.mk m₁ m₃ (v₂₃ ≫ w₁₂) ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) (-1))
      (Triangle.mk o.m₁ o.m₃
        ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk m₁ m₃ (v₂₃ ≫ w₁₂))

Tactic:
apply isomorphic_distinguished _ ((Triangle.shift_distinguished_iff _ (-1 : ℤ)).mpr o.mem)

Premises used: CategoryTheory.Triangulated.Octahedron.mem, Iff.mpr, CategoryTheory.Pretriangulated.Triangle.shift_distinguished_iff, CategoryTheory.Pretriangulated.isomorphic_distinguished, OfNat.ofNat, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_5 :
  (Triangle.mk m₁ m₃ (v₂₃ ≫ w₁₂)).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.symm (shiftShiftNeg Z₁₂ 1))) =
    Iso.hom (Iso.symm (shiftShiftNeg Z₂₃ 1)) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) (-1))
          (Triangle.mk o.m₁ o.m₃
            ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁) ≫
              Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃))).mor₃
⊢ Triangle.mk m₁ m₃ (v₂₃ ≫ w₁₂) ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) (-1))
      (Triangle.mk o.m₁ o.m₃
        ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃))

Tactic:
refine Triangle.isoMk _ _ (shiftShiftNeg Z₁₂ (1 : ℤ)).symm
      (-(shiftShiftNeg Z₁₃ (1 : ℤ)).symm) (shiftShiftNeg Z₂₃ (1 : ℤ)).symm (comm₃ := ?_)

Premises used: CategoryTheory.Pretriangulated.Triangle.isoMk
-- 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
A : 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
rw :
  ∀ (x₂ : (↑(ShortComplex.X₂ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : Type v_1)),
    Eq (α :=
        (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
                (ShortComplex.g ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
              (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1)) →
                (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₃ : Type v_1))
            x₂ :
          (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : Type v_1))
        (0 :
          (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : Type v_1)) →
      ∃ (x₁ :
        (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
                (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
              (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
                (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1))
            x₁ =
          x₂
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))

Tactic:
rw [ShortComplex.ab_exact_iff]

Premises used: CategoryTheory.ShortComplex.ab_exact_iff
-- 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
A : 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
x₂ : unop A ⟶ T.obj₂
x₃ :
  ∀ (hx₂ : x₂ ≫ T.mor₂ = 0),
    ∃ (x₁ :
      (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
              (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
            (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
              (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1))
          x₁ =
        x₂
⊢ Eq (α := (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
              (ShortComplex.g ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
            (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1)) →
              (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₃ : Type v_1))
          x₂ :
        (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : Type v_1))
      (0 :
        (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : Type v_1)) →
    ∃ (x₁ :
      (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
              (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
            (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
              (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1))
          x₁ =
        x₂

Tactic:
(hx₂ : x₂ ≫ T.mor₂ = 0)
-- 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
A : 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
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
obtain :
  ∀ (x₁ : unop A ⟶ T.obj₁) (hx₁ : x₂ = x₁ ≫ T.mor₁),
    ∃ (x₁ :
      (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
              (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
            (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
              (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1))
          x₁ =
        x₂
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂ : Type v_1))
        x₁ =
      x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := T.coyoneda_exact₂ hT x₂ hx₂

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂
-- 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
A : 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
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
x₁ : unop A ⟶ T.obj₁
hx₁ : x₂ = x₁ ≫ T.mor₁
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).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
A : 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
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
x₁ : unop A ⟶ T.obj₁
hx₁ : x₂ = x₁ ≫ T.mor₁
⊢ ∃ (x₁ : (↑(ShortComplex.X₁ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) : 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 preadditiveCoyoneda A)))
            (ShortComplex.f ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))) :
          (a : (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₁ : Type v_1)) →
            (↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).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
B : C
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    T
rw :
  ∀ (x₂ : (↑(ShortComplex.X₂ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)),
    Eq (α := (↑(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.g ((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₂ :
          (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1))
        (0 :
          (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)) →
      ∃ (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₂
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))

Tactic:
rw [ShortComplex.ab_exact_iff]

Premises used: CategoryTheory.ShortComplex.ab_exact_iff
-- 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
x₃ :
  ∀ (hx₂ : T.mor₂.unop ≫ x₂ = 0),
    ∃ (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₂
⊢ Eq (α := (↑(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.g ((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₂ :
        (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1))
      (0 : (↑(ShortComplex.X₃ ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))) : Type v_1)) →
    ∃ (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:
(hx₂ : T.mor₂.unop ≫ x₂ = 0)