mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
⊢ (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
⊢ (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
⊢ P.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
⊢ P.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
r : Retract X Y
hY : ∃ n, P.triangEnvelopeIter n Y
⊢ ∃ n, P.triangEnvelopeIter n X

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
r : Retract X Y
hY : ∃ n, P.triangEnvelopeIter n Y
⊢ ∃ n, P.triangEnvelopeIter n X
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
r : Retract X Y
n : ℕ
hn : P.triangEnvelopeIter n Y
⊢ ∃ n, P.triangEnvelopeIter n X

Tactic:
exact ⟨n, IsStableUnderRetracts.of_retract r hn⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
hX : ∃ n, P.triangEnvelopeIter n X
⊢ P.triangEnvelope.shift a X

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
hX : ∃ n, P.triangEnvelopeIter n X
⊢ P.triangEnvelope.shift a X
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ n, P.triangEnvelopeIter n ((shiftFunctor C a).obj X)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ n, P.triangEnvelopeIter n ((shiftFunctor C a).obj X)
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : ∃ n, P.triangEnvelopeIter n T.obj₁
h₂ : ∃ n, P.triangEnvelopeIter n T.obj₃
⊢ ∃ n, P.triangEnvelopeIter n T.obj₂

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : ∃ n, P.triangEnvelopeIter n T.obj₁
h₂ : ∃ n, P.triangEnvelopeIter n T.obj₃
⊢ ∃ n, P.triangEnvelopeIter n T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: case h
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
⊢ ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂

Tactic:
]

Goal state after:
case h
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
⊢ ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
⊢ ∀ (i : ℕ), P.triangEnvelopeIter i ≤ Q

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
⊢ ∀ (i : ℕ), P.triangEnvelopeIter i ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((commShiftIso F m).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X))) ≫
          (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
            ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((commShiftIso F m).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X))) ≫
          (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
            ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ P ≤ Q

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ P ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
hn : P.triangEnvelopeIter n = ⊤
⊢ ⊤ ≤ P.triangEnvelope

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
hn : P.triangEnvelopeIter n = ⊤
⊢ ⊤ ≤ P.triangEnvelope
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).op.obj (op (F.obj (unop X))))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
]

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).op.obj (op (F.obj (unop X))))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ adj.unit.app Z ≫ G.map h = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X ≫ (commShiftIso F.op n).hom.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X ≫ (commShiftIso F.op n).hom.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
eq' : G.map T.mor₁ ≫ f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
          ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
          ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case left
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ₁ φ₂ : Y ⟶ Z
hφ : (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₁ = (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₂
⊢ φ₁ ≫ (adj.homEquiv Z T.obj₃) h = φ₂ ≫ (adj.homEquiv Z T.obj₃) h

Tactic:
]

Goal state after:
case left
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ₁ φ₂ : Y ⟶ Z
hφ : (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₁ = (fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h) φ₂
⊢ φ₁ ≫ (adj.homEquiv Z T.obj₃) h = φ₂ ≫ (adj.homEquiv Z T.obj₃) h
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj (F.op.mapTriangle.obj T)) ∈ Pretriangulated.distinguishedTriangles

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj (F.op.mapTriangle.obj T)) ∈ Pretriangulated.distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles