awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
h₂ :
  Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₂) ⟶ op (F.obj (unop Y).obj₂))
    ((F.map f.unop.hom₂).op ≫ 𝟙 (op (F.obj (unop Y).obj₂))) (𝟙 (op (F.obj (unop X).obj₂)) ≫ (F.map f.unop.hom₂).op)
⊢ Eq (α :=
    Triangle.obj₂ (obj (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) X) ⟶
      Triangle.obj₂ (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) Y))
    (TriangleMorphism.hom₂
      (map (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) f ≫
        Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            Y)))
    (TriangleMorphism.hom₂
      (Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            X) ≫
        map (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
h₃ :
  Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₁) ⟶ op (F.obj (unop Y).obj₁))
    ((F.map f.unop.hom₁).op ≫ 𝟙 (op (F.obj (unop Y).obj₁))) (𝟙 (op (F.obj (unop X).obj₁)) ≫ (F.map f.unop.hom₁).op)
⊢ Eq (α :=
    Triangle.obj₃ (obj (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) X) ⟶
      Triangle.obj₃ (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) Y))
    (TriangleMorphism.hom₃
      (map (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) f ≫
        Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            Y)))
    (TriangleMorphism.hom₃
      (Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            X) ≫
        map (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
⊢ Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₃) ⟶ op (F.obj (unop Y).obj₃))
    ((F.map f.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y).obj₃))) (𝟙 (op (F.obj (unop X).obj₃)) ≫ (F.map f.unop.hom₃).op)

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
⊢ Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₂) ⟶ op (F.obj (unop Y).obj₂))
    ((F.map f.unop.hom₂).op ≫ 𝟙 (op (F.obj (unop Y).obj₂))) (𝟙 (op (F.obj (unop X).obj₂)) ≫ (F.map f.unop.hom₂).op)

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
⊢ Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₁) ⟶ op (F.obj (unop Y).obj₁))
    ((F.map f.unop.hom₁).op ≫ 𝟙 (op (F.obj (unop Y).obj₁))) (𝟙 (op (F.obj (unop X).obj₁)) ≫ (F.map f.unop.hom₁).op)

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
T : Triangle.{v_1, u_1} Cᵒᵖ
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
rw :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
    (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
    (unop (obj (Equivalence.inverse (triangleOpEquivalence D)) (obj F.op.mapTriangle T)))
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} Dᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite D) ⋯ _) (obj F.op.mapTriangle T)

Tactic:
rw [mem_distTriang_op_iff]

Premises used: CategoryTheory.Pretriangulated.mem_distTriang_op_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
T : Triangle.{v_1, u_1} Cᵒᵖ
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
    (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
    (unop (obj (Equivalence.inverse (triangleOpEquivalence D)) (obj F.op.mapTriangle T)))

Tactic:
Pretriangulated.isomorphic_distinguished _
      ((F.map_distinguished _ (unop_distinguished _ dT))) _
      (((opMapTriangleCompTriangleOpEquivalenceInverse F).symm.app T).unop)

Premises used: CategoryTheory.Functor.opMapTriangleCompTriangleOpEquivalenceInverse, CategoryTheory.Pretriangulated.unop_distinguished, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.map_distinguished, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
T : Triangle.{v_1, u_1} Cᵒᵖ
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
    (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
    (unop (obj (Equivalence.inverse (triangleOpEquivalence D)) (obj F.op.mapTriangle T)))

Tactic:
exact Pretriangulated.isomorphic_distinguished _
      ((F.map_distinguished _ (unop_distinguished _ dT))) _
      (((opMapTriangleCompTriangleOpEquivalenceInverse F).symm.app T).unop)

Premises used: CategoryTheory.Functor.opMapTriangleCompTriangleOpEquivalenceInverse, CategoryTheory.Pretriangulated.unop_distinguished, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.map_distinguished, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.op.IsTriangulated
T : Triangle.{v_1, u_1} C
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_5 _ inst_6 inst_7 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop (obj (𝟭 (Triangle.{v_2, u_2} D)ᵒᵖ) (op (obj F.mapTriangle T))))

Tactic:
have := distinguished_iff_of_iso ((triangleOpEquivalence D).unitIso.app
      (Opposite.op (F.mapTriangle.obj T))).unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.op.IsTriangulated
T : Triangle.{v_1, u_1} C
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_5 _ inst_6 inst_7 _) T
this :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop (obj (𝟭 (Triangle.{v_2, u_2} D)ᵒᵖ) (op (obj F.mapTriangle T))))
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) (obj F.mapTriangle T)

Tactic:
rw [Functor.id_obj, Opposite.unop_op (F.mapTriangle.obj T)] at this

Premises used: CategoryTheory.Functor.mapTriangle, CategoryTheory.Functor.id_obj, Opposite.unop_op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.op.IsTriangulated
T : Triangle.{v_1, u_1} C
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_5 _ inst_6 inst_7 _) T
this :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) (obj F.mapTriangle T)
rw :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} Dᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite D) ⋯ _)
    (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) (op T))
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
    (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) (obj F.mapTriangle T)

Tactic:
rw [← this, Functor.comp_obj, ← mem_distTriang_op_iff, ← Functor.op_obj, ← Functor.comp_obj,
      distinguished_iff_of_iso ((mapTriangleOpCompTriangleOpEquivalenceFunctor F).app
      (Opposite.op T))]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Pretriangulated.mem_distTriang_op_iff, Opposite.op, CategoryTheory.Pretriangulated.distinguished_iff_of_iso, CategoryTheory.Iso.app, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.op.IsTriangulated
T : Triangle.{v_1, u_1} C
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_5 _ inst_6 inst_7 _) T
this :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) (obj F.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} Dᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite D) ⋯ _)
    (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) (op T))

Tactic:
F.op.map_distinguished _ (op_distinguished _ dT)

Premises used: CategoryTheory.Functor.op, Set.Mem, CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.Functor.map_distinguished, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.op.IsTriangulated
T : Triangle.{v_1, u_1} C
dT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_5 _ inst_6 inst_7 _) T
this :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _)
      (unop
        (obj (Equivalence.functor (triangleOpEquivalence D) ⋙ Equivalence.inverse (triangleOpEquivalence D))
          (op (obj F.mapTriangle T)))) ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D))
      (@Pretriangulated.distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) (obj F.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} Dᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite D) ⋯ _)
    (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) (op T))

Tactic:
exact F.op.map_distinguished _ (op_distinguished _ dT)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
⊢ F.op.IsTriangulated ↔ F.IsTriangulated

Tactic:
⟨fun _ ↦ F.isTriangulated_of_op, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Functor.isTriangulated_of_op, Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    unop (Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) Y) ⟶
      unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X))
    (Quiver.Hom.unop
      (Functor.map (shiftFunctor C n ⋙ opOp C) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Iso.op (Iso.app (shiftFunctorOpIso C (-n) n ⋯) (op X)) ≪≫
                  Iso.app (Iso.symm (shiftFunctorOpIso Cᵒᵖ n (-n) ⋯)) (op (op X)) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ≅
                  Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X))
            Y)))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : C) ↦
              (Iso.op (Iso.app (shiftFunctorOpIso C (-n) n ⋯) (op X)) ≪≫
                  Iso.app (Iso.symm (shiftFunctorOpIso Cᵒᵖ n (-n) ⋯)) (op (op X)) :
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ opOp C) X ≅
                  Functor.obj.{v_1, v_1, u_1, u_1} (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) X))
            X) ≫
        Functor.map (opOp C ⋙ shiftFunctor Cᵒᵖᵒᵖ n) f))

Tactic:
simp [shiftFunctor_op_map _ n (-n), shiftFunctor_op_map _ (-n) n]

Premises used: CategoryTheory.Pretriangulated.shiftFunctor_op_map, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) iso_hom_app._auto_1
⊢ m + n = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia