awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveCoyoneda A))
have 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₂
Tactic: rw [ShortComplex.ab_exact_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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₂
⊢ 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₂
have 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₂
Tactic: (hx₂ : x₂ ≫ T.mor₂ = 0)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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₁ : (↑(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₂
have 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₂
Tactic: obtain ⟨x₁, hx₁⟩ := T.coyoneda_exact₂ hT x₂ hx₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map (Functor.obj preadditiveYoneda B))
have 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₂
Tactic: rw [ShortComplex.ab_exact_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ 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₂
have 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₂
Tactic: (hx₂ : T.mor₂.unop ≫ x₂ = 0)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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₁ : (↑(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₂
have 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₂
Tactic: obtain ⟨x₃, hx₃⟩ := Triangle.yoneda_exact₂ _ (unop_distinguished T hT) x₂ hx₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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))
    ((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')
have 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 sorry)
  ((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: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ (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
have 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₁ sorry)) B) =
  (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ 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
have 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₃
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
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
⊢ (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₃
have 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)
Tactic: apply (ShiftedHom.opEquiv _).injective