mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ x✝¹)).hom.app x✝ ≫
        (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) x✝¹).map (τ.app x✝) =
    F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      τ.app ((shiftFunctor C (φ x✝¹)).obj x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app x✝ ≫ (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj x✝)

Tactic:
]

Goal state after:
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
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ x✝¹)).hom.app x✝ ≫
        (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) x✝¹).map (τ.app x✝) =
    F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      τ.app ((shiftFunctor C (φ x✝¹)).obj x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app x✝ ≫ (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj x✝)
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) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
]

Goal state after:
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) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
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₂
⊢ ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁

Tactic:
]

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
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId C (-a) a ⋯).hom.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          (𝟭 C).map ((Functor.commShiftIso G a).inv.app (F.obj X✝)) ≫ (Functor.commShiftIso G a).hom.app (F.obj X✝)

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
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
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId C (-a) a ⋯).hom.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          (𝟭 C).map ((Functor.commShiftIso G a).inv.app (F.obj X✝)) ≫ (Functor.commShiftIso G a).hom.app (F.obj X✝)
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ᵒᵖ
⊢ 𝟙 (Opposite.op ((shiftFunctor C (-1)).obj 0)) = 0

Tactic:
]

Goal state after:
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ᵒᵖ
⊢ 𝟙 (Opposite.op ((shiftFunctor C (-1)).obj 0)) = 0
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
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

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
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
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
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ᵒᵖ
⊢ 0 = 0

Tactic:
]

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
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
    (Functor.CommShift.isoAdd (Functor.commShiftIso G a) (Functor.commShiftIso G b))

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
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
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
    (Functor.CommShift.isoAdd (Functor.commShiftIso G a) (Functor.commShiftIso G b))
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ᵒᵖ
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
]

Goal state after:
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ᵒᵖ
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
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
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂

Tactic:
]

Goal state after:
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
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂
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
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂

Tactic:
]

Goal state after:
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
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ T.mor₃ ≫ 𝟙 ((shiftFunctor Cᵒᵖ 1).obj ((𝟭 Cᵒᵖ).obj T.obj₁)) = T.mor₃

Tactic:
]

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ T.mor₃ ≫ 𝟙 ((shiftFunctor Cᵒᵖ 1).obj ((𝟭 Cᵒᵖ).obj T.obj₁)) = T.mor₃
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₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃

Tactic:
]

Goal state after:
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₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: case e_a.e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = (ShiftedHom.opEquiv 1) T.mor₃

Tactic:
]

Goal state after:
case e_a.e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = (ShiftedHom.opEquiv 1) T.mor₃
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✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (op T)) n₀ n₁ h))
      x =
    T.mor₃ ≫ (shiftFunctor C 1).map x ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Tactic:
simp only [Functor.homologySequenceδ, preadditiveYoneda_shiftMap_apply,
    ShiftedHom.comp, ← Category.assoc]
  congr 2
  apply (ShiftedHom.opEquiv _).injective
  rw [Equiv.apply_symm_apply]
  rfl

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₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (((shiftFunctor C 1).map
              ((shiftFunctor Cᵒᵖ 1).map (a ≫ (opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁)).unop).op ≫
          (opShiftFunctorEquivalence C 1).unitIso.inv.app
            (Opposite.op ((shiftFunctor C 1).obj (Opposite.unop ((shiftFunctor Cᵒᵖ 1).obj T₂.obj₁))))).unop ≫
      (shiftFunctor C 1).map T₁.mor₃.unop

Tactic:
]

Goal state after:
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₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (((shiftFunctor C 1).map
              ((shiftFunctor Cᵒᵖ 1).map (a ≫ (opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁)).unop).op ≫
          (opShiftFunctorEquivalence C 1).unitIso.inv.app
            (Opposite.op ((shiftFunctor C 1).obj (Opposite.unop ((shiftFunctor Cᵒᵖ 1).obj T₂.obj₁))))).unop ≫
      (shiftFunctor C 1).map T₁.mor₃.unop
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
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
]

Goal state after:
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
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ y.app X ≫ x.app X = x.app X ≫ y.app X

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ y.app X ≫ x.app X = x.app X ≫ y.app X
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ y.app X ≫ x.app X = y.app X ≫ x.app X

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.hom ≫ (↑z * ↑z⁻¹).app Y ≫ e.inv = 𝟙 X

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.hom ≫ (↑z * ↑z⁻¹).app Y ≫ e.inv = 𝟙 X
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.inv ≫ (↑z⁻¹ * ↑z).app X ≫ e.hom = 𝟙 Y

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.inv ≫ (↑z⁻¹ * ↑z).app X ≫ e.hom = 𝟙 Y
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ e.hom ≫ π.f i = e.hom ≫ α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ e.hom ≫ π.f i = e.hom ≫ α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      homologyπ ((singleFunctor C i).obj P) i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      homologyπ ((singleFunctor C i).obj P) i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ cyclesMap π i ≫ iCycles ((single C (ComplexShape.up ℤ) i).obj P) i =
    cyclesMap π i ≫ ((single C (ComplexShape.up ℤ) i).obj P).iCycles i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ a • 𝟙 X, naturality := ⋯ }

Tactic:
]

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ a • 𝟙 X, naturality := ⋯ }
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X = (a * b) • 𝟙 X ≫ 𝟙 X

Tactic:
]

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X = (a * b) • 𝟙 X ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
a : R
f : X ⟶ Y
⊢ (φ a).app X ≫ f = f ≫ (φ a).app Y

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
a : R
f : X ⟶ Y
⊢ (φ a).app X ≫ f = f ≫ (φ a).app Y
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ 𝟙 (((single C (ComplexShape.up ℤ) i).obj P).X i) = 𝟙 (((singleFunctor C i).obj P).X i)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ 𝟙 (((single C (ComplexShape.up ℤ) i).obj P).X i) = 𝟙 (((singleFunctor C i).obj P).X i)