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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (Triangle.mk (Opposite.unop T₁).mor₂.op (Opposite.unop T₁).mor₁.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
            (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₁).mor₃.op)).mor₃ ≫
      (shiftFunctor Cᵒᵖ 1).map φ.unop.hom₃.op =
    φ.unop.hom₁.op ≫
      (Triangle.mk (Opposite.unop T₂).mor₂.op (Opposite.unop T₂).mor₁.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
            (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op)).mor₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ IsIso (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₂ : R₂.Exact
hR₁' : Epi R₁.g
h₀ : Epi φ.τ₁
h₁ : Mono φ.τ₂
⊢ R₁.toComposableArrows.map' 0 2 Abelian.mono_of_epi_of_mono_of_mono'._proof_2
      Abelian.mono_of_epi_of_epi_mono'._proof_1 =
    0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono R₂.f
h₀ : Epi φ.τ₂
h₁ : Mono φ.τ₃
⊢ R₂.toComposableArrows.map' 0 2 Abelian.mono_of_epi_of_mono_of_mono'._proof_2
      Abelian.mono_of_epi_of_epi_mono'._proof_1 =
    0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁷ : AddMonoid A
inst✝⁶ : AddMonoid B
inst✝⁵ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasShift D B
F : C ⥤ D
inst✝² : F.CommShift B
G : C ⥤ D
inst✝¹ : G.CommShift B
τ : F ⟶ G
inst✝ : CommShift τ B
x✝ : A
⊢ (commShiftIso (PullbackShift.functor φ F) x✝).hom ≫
      whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift D φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natTrans φ τ) ≫
      (commShiftIso (PullbackShift.functor φ G) x✝).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((Triangle.mk T₂.mor₂.unop T₂.mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫
              (shiftFunctor C 1).map T₂.mor₃.unop)).mor₃ ≫
        (shiftFunctor C 1).map φ.hom₃.unop).op =
    (φ.hom₁.unop ≫
        (Triangle.mk T₁.mor₂.unop T₁.mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫
              (shiftFunctor C 1).map T₁.mor₃.unop)).mor₃).op

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ : Triangle Cᵒᵖ
hT₁ : T₁ ∈ distinguishedTriangles C
T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝³ : Category.{v_2, u_4} D
inst✝² : HasShift D B
F : C ⥤ D
inst✝¹ : F.CommShift B
G : C ⥤ D
inst✝ : G.CommShift B
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (PullbackShift C φ)) x✝).hom ≫
      Functor.whiskerRight (PullbackShift.natIsoId C φ).hom (shiftFunctor (PullbackShift C φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoId C φ).hom ≫
      (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
⊢ CommShift.CompatibilityUnit adj (iso adj a) (Functor.commShiftIso G a)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
          (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
            (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₁ ≫
      (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₂).hom =
    (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₁).hom ≫
      (Opposite.unop T).mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ iso adj 0 = Functor.CommShift.isoZero F A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ IsZero ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).obj₃

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₁ ≫ (Iso.refl (contractibleTriangle X).obj₂).hom =
    (Iso.refl (contractibleTriangle X).obj₁).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a b : A
⊢ iso adj (a + b) = Functor.CommShift.isoAdd (iso adj a) (iso adj b)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
          (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
            (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₂ ≫
      (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₃).hom =
    (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₂).hom ≫
      (Opposite.unop T).mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₂ ≫ (⋯.iso ⋯).hom =
    (Iso.refl (contractibleTriangle X).obj₂).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ adj.CommShift A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl (contractibleTriangle X).obj₁).hom =
    (⋯.iso ⋯).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₃

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ ((Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
              (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₃ ≫
        (shiftFunctor C 1).map
          (Iso.refl
              (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₁).hom).op =
    ((Iso.refl
            (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
                (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                  (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₃).hom ≫
        (Opposite.unop T).mor₃).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').functor.CommShift A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ contractibleTriangle X ∈ distinguishedTriangles C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').inverse.CommShift A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₁ ≫
      (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₂).hom =
    (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₁).hom ≫
      (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.functor.CommShift A
⊢ E.CommShift A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ ((Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₂ ≫
        (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop).hom).op =
    ((Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₂).hom ≫
        (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₂).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.inverse.CommShift A
⊢ E.CommShift A

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₁).hom =
    (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop).hom ≫
      (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₃

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
f : T₁ ⟶ T₂
⊢ ((𝟭 (Triangle C)ᵒᵖ).map f ≫
        ((Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).isoMk
              (Opposite.unop T₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom).unop =
    (((Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).isoMk
              (Opposite.unop T₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom ≫
        (functor C ⋙ inverse C).map f).unop

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).Exact

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).Exact

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ (shiftFunctor C n₀).obj T.obj₃
⊢ 1 + n₀ = n₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₁ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₁).hom ≫
      (Triangle.mk g f.unop h).mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ (shiftFunctor C n₀).obj T.obj₃
⊢ (ConcreteCategory.hom ((preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h)) x =
    x ≫ (shiftFunctor C n₀).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₂ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₃).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom ≫
      (Triangle.mk g f.unop h).mor₂

Tactic:
by

Goal state after: