awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Eq (α :=
    Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop (Triangle.mk u₁₂ v₁₂ w₁₂).obj₃)) ⟶
      Opposite.op (Opposite.unop (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
          Opposite.unop
            (Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.inverse (opShiftFunctorEquivalence C 1))
              (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
              (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) o.m₃))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃.unop)))

Tactic:
have eq₃ := congr($(o.comm₃).op)
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶ X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) o.m₃) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop) ≫
      NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁)
⊢ Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₁₃.unop ≫ o.m₃)))
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop))

Tactic:
rw [← Category.assoc, ← op_comp, ← Functor.map_comp,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso] at eq₃

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Equivalence.unitIso, CategoryTheory.NatIso.cancel_natIso_inv_right, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₁₃.unop ≫ o.m₃)))
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop))
⊢ o.m₃.op ≫ w₁₃ = w₁₂

Tactic:
congr($(Functor.map_injective _ congr($(eq₃).unop)).op)

Premises used: congrArg, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shiftFunctor, id, CategoryTheory.Functor.map_injective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₁₃.unop ≫ o.m₃)))
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop))
⊢ o.m₃.op ≫ w₁₃ = w₁₂

Tactic:
exact congr($(Functor.map_injective _ congr($(eq₃).unop)).op)
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Eq (α :=
    Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop (Triangle.mk u₁₃ v₁₃ w₁₃).obj₃)) ⟶
      Opposite.op (Opposite.unop (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
          Opposite.unop
            (Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.inverse (opShiftFunctorEquivalence C 1))
              (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
              (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃.unop) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) o.m₁))
    (Quiver.Hom.op
      ((Triangle.mk u₁₂ v₁₂ w₁₂).mor₁.unop ≫
        CategoryStruct.comp (Y :=
          Opposite.unop
            (Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.inverse (opShiftFunctorEquivalence C 1))
              (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
              (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop)))

Tactic:
have eq₂ := congr($(o.comm₂).op)
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  Eq (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶ X₂)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) o.m₁) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₂₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₂)
    ((Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁) ≫
      u₁₂)
⊢ Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₂)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₂₃.unop ≫ o.m₁)))
    (Quiver.Hom.op
      (Functor.map (shiftFunctor C (A := ℤ) 1)
        (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂) ≫ w₁₃.unop)))

Tactic:
rw [← Category.assoc, ← op_comp, ← Functor.map_comp, Category.assoc,
        ← opShiftFunctorEquivalence_unitIso_inv_naturality, ← Category.assoc,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso, ← op_comp,
        ← Functor.map_comp] at eq₂

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Equivalence.unitIso, CategoryTheory.NatIso.cancel_natIso_inv_right, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₂)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₂₃.unop ≫ o.m₁)))
    (Quiver.Hom.op
      (Functor.map (shiftFunctor C (A := ℤ) 1)
        (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂) ≫ w₁₃.unop)))
⊢ w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
congr($(Functor.map_injective _ congr($(eq₂).unop)).op).symm

Premises used: congrArg, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shiftFunctor, id, CategoryTheory.Functor.map_injective, OfNat.ofNat, Eq.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  Eq (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₂)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₂₃.unop ≫ o.m₁)))
    (Quiver.Hom.op
      (Functor.map (shiftFunctor C (A := ℤ) 1)
        (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂) ≫ w₁₃.unop)))
⊢ w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
exact congr($(Functor.map_injective _ congr($(eq₂).unop)).op).symm

Premises used: congrArg, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shiftFunctor, id, CategoryTheory.Functor.map_injective, OfNat.ofNat, Eq.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{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
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
      (Opposite.op
        (Triangle.mk o.m₁ o.m₃
          ((Triangle.mk u₁₂ v₁₂ w₁₂).mor₂.unop ≫
            CategoryStruct.comp (Y :=
              Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1}
                  (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                    Equivalence.inverse (opShiftFunctorEquivalence C 1))
                  (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                  (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
              (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃.unop)))))

Tactic:
have := op_distinguished _ o.mem
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
Y : C
hY : P.rightOrthogonal Y
X : C
f : X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y
hX : P X
obtain :
  ∀ (g : Functor.obj.{v, v, u, u} (Equivalence.functor (Equivalence.symm (shiftEquiv C n))) X ⟶ Y),
    Eq (α := X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)
      ((Adjunction.homEquiv (Equivalence.toAdjunction (Equivalence.symm (shiftEquiv C n))) X Y :
            (a : (shiftEquiv C n).symm.functor.obj X ⟶ Y) → X ⟶ (shiftEquiv C n).symm.inverse.obj Y)
          g :
        X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (Equivalence.symm (shiftEquiv C n))) Y)
      (0 : X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := ((shiftEquiv C n).symm.toAdjunction.homEquiv _ _).surjective f

Premises used: CategoryTheory.shiftEquiv, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.surjective, CategoryTheory.Equivalence.symm, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
Y : C
hY : P.rightOrthogonal Y
X : C
hX : P X
g : Functor.obj.{v, v, u, u} (Equivalence.functor (Equivalence.symm (shiftEquiv C n))) X ⟶ Y
⊢ Eq (α := X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)
    ((Adjunction.homEquiv (Equivalence.toAdjunction (Equivalence.symm (shiftEquiv C n))) X Y :
          (a : (shiftEquiv C n).symm.functor.obj X ⟶ Y) → X ⟶ (shiftEquiv C n).symm.inverse.obj Y)
        g :
      X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (Equivalence.symm (shiftEquiv C n))) Y)
    (0 : X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)

Tactic:
simp [hY g (P.le_shift (-n) _ hX), Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, Neg.neg, CategoryTheory.ObjectProperty.le_shift