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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₁ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.mk h f' g').invRotate.invRotate.mor₁

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).mor₂ ≫
      (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₃).hom =
    (Iso.refl (Triangle.mk (((shiftEquiv C 1).unitIso.app X).hom ≫ T'.mor₁) T'.mor₂ h).obj₂).hom ≫
      (Triangle.mk h f' g').invRotate.invRotate.mor₂

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      ((CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C b).map
            (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)

Tactic:
Functor.map_units_smul,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      ((CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (a.negOnePow •
            (CategoryTheory.shiftFunctor C b).map
              ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁)) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (rotate C ⋙ rotate C ⋙ rotate C).map f ≫
        (((rotate C ⋙ rotate C ⋙ rotate C).obj Y).isoMk ((Triangle.shiftFunctor C 1).obj Y)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₁)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₂)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((rotate C ⋙ rotate C ⋙ rotate C).obj X).isoMk ((Triangle.shiftFunctor C 1).obj X)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₁)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₂)
            (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (Triangle.shiftFunctor C 1).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (invRotate C ⋙ invRotate C ⋙ invRotate C).map f ≫
        (((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).isoMk ((Triangle.shiftFunctor C (-1)).obj Y)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₁)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₂)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).isoMk ((Triangle.shiftFunctor C (-1)).obj X)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₁)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₂)
            (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (Triangle.shiftFunctor C (-1)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ : Cocycle K L n
⊢ (fun γ ↦ γ.rightUnshift n hn') ((fun γ ↦ γ.rightShift a n' hn') γ) = γ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ : Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
⊢ (fun γ ↦ γ.rightShift a n' hn') ((fun γ ↦ γ.rightUnshift n hn') γ) = γ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n' + a = n
γ γ' : Cocycle K L n
⊢ (γ + γ').rightShift a n' hn' = γ.rightShift a n' hn' + γ'.rightShift a n' hn'

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ : Cocycle K L n
⊢ (fun γ ↦ γ.leftUnshift n hn') ((fun γ ↦ γ.leftShift a n' hn') γ) = γ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
⊢ (fun γ ↦ γ.leftShift a n' hn') ((fun γ ↦ γ.leftUnshift n hn') γ) = γ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n a n' : ℤ
hn' : n + a = n'
γ γ' : Cocycle K L n
⊢ (γ + γ').leftShift a n' hn' = γ.leftShift a n' hn' + γ'.leftShift a n' hn'

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ T.mor₁ ≫ f = 0 ≫ (mk 0 (𝟙 X) 0).mor₁

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ (contractibleTriangle X).mor₂ ≫ 0 = f ≫ T.mor₂

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ (CategoryTheory.shiftFunctor C 1).obj T.obj₁
hf : f ≫ (CategoryTheory.shiftFunctor C 1).map T.mor₁ = 0
⊢ f ≫ T.rotate.rotate.mor₂ = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Mono f
X : C
g : X ⟶ X✝
h : Y✝ ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk g f h ∈ distinguishedTriangles
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0

Tactic:
rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Tactic:
by
  have : Mono φ.hom₂ := by
    rw [mono_iff_cancel_zero]
    intro A f hf
    obtain ⟨g, rfl⟩ := Triangle.coyoneda_exact₂ _ hT f
      (by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])
    rw [assoc] at hf
    obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])
    obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g := by
      refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
      have eq := ((invRotate C).map φ).comm₁
      dsimp only [invRotate] at eq
      rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
    erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
  refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)
  · intro f₁ f₂ h
    simpa only [← cancel_mono φ.hom₂] using h
  · intro y₂
    obtain ⟨x₃, hx₃⟩ : ∃ (x₃ : A ⟶ T.obj₃), x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂ :=
      ⟨y₂ ≫ T'.mor₂ ≫ inv φ.hom₃, by simp⟩
    obtain ⟨x₂, hx₂⟩ := Triangle.coyoneda_exact₃ _ hT x₃
      (by rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        comp_distTriang_mor_zero₂₃ _ hT', comp_zero])
    obtain ⟨y₁, hy₁⟩ := Triangle.coyoneda_exact₂ _ hT' (y₂ - x₂ ≫ φ.hom₂)
      (by rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, sub_self])
    obtain ⟨x₁, hx₁⟩ : ∃ (x₁ : A ⟶ T.obj₁), x₁ ≫ φ.hom₁ = y₁ := ⟨y₁ ≫ inv φ.hom₁, by simp⟩
    refine ⟨x₂ + x₁ ≫ T.mor₁, ?_⟩
    dsimp
    rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem : Triangle.mk g h 0 ∈ distinguishedTriangles
e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ (Triangle.mk g h 0).mor₁ ≫ e.hom = (Iso.refl (Triangle.mk g h 0).obj₁).hom ≫ (binaryBiproductTriangle X₁ X₂).mor₁

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem : Triangle.mk g h 0 ∈ distinguishedTriangles
e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ (Triangle.mk g h 0).mor₂ ≫ (Iso.refl (Triangle.mk g h 0).obj₃).hom = e.hom ≫ (binaryBiproductTriangle X₁ X₂).mor₂

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0

Tactic:
by
      have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 := by
        rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]
      rw [φ'.comm₂_assoc, h₂, id_comp] at this
      simpa using this

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : HasShift C ℤ
inst✝⁵ : HasShift D ℤ
inst✝⁴ : HasShift E ℤ
F : C ⥤ D
inst✝³ : F.CommShift ℤ
G : D ⥤ E
inst✝² : G.CommShift ℤ
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Triangle C
f : F.mapTriangle.obj X ⟶ F.mapTriangle.obj Y
⊢ F.mapTriangle.map
      { hom₁ := F.preimage f.hom₁, hom₂ := F.preimage f.hom₂, hom₃ := F.preimage f.hom₃, comm₁ := ⋯, comm₂ := ⋯,
        comm₃ := ⋯ } =
    f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
n : ℤ
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (Triangle.shiftFunctor C n ⋙ F.mapTriangle).map f ≫
        (((Triangle.shiftFunctor C n ⋙ F.mapTriangle).obj Y).isoMk ((F.mapTriangle ⋙ Triangle.shiftFunctor D n).obj Y)
            ((commShiftIso F n).app Y.obj₁) ((commShiftIso F n).app Y.obj₂) ((commShiftIso F n).app Y.obj₃) ⋯ ⋯ ⋯).hom =
      (((Triangle.shiftFunctor C n ⋙ F.mapTriangle).obj X).isoMk ((F.mapTriangle ⋙ Triangle.shiftFunctor D n).obj X)
            ((commShiftIso F n).app X.obj₁) ((commShiftIso F n).app X.obj₂) ((commShiftIso F n).app X.obj₃) ⋯ ⋯ ⋯).hom ≫
        (F.mapTriangle ⋙ Triangle.shiftFunctor D n).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (F.mapTriangle ⋙ rotate D).map f ≫
        (((F.mapTriangle ⋙ rotate D).obj Y).isoMk ((rotate C ⋙ F.mapTriangle).obj Y)
            (Iso.refl ((F.mapTriangle ⋙ rotate D).obj Y).obj₁) (Iso.refl ((F.mapTriangle ⋙ rotate D).obj Y).obj₂)
            ((commShiftIso F 1).symm.app Y.obj₁) ⋯ ⋯ ⋯).hom =
      (((F.mapTriangle ⋙ rotate D).obj X).isoMk ((rotate C ⋙ F.mapTriangle).obj X)
            (Iso.refl ((F.mapTriangle ⋙ rotate D).obj X).obj₁) (Iso.refl ((F.mapTriangle ⋙ rotate D).obj X).obj₂)
            ((commShiftIso F 1).symm.app X.obj₁) ⋯ ⋯ ⋯).hom ≫
        (rotate C ⋙ F.mapTriangle).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (F.mapTriangle ⋙ invRotate D).map f ≫
        (((F.mapTriangle ⋙ invRotate D).obj Y).isoMk ((invRotate C ⋙ F.mapTriangle).obj Y)
            ((commShiftIso F (-1)).symm.app Y.obj₃) (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj Y).obj₂)
            (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((F.mapTriangle ⋙ invRotate D).obj X).isoMk ((invRotate C ⋙ F.mapTriangle).obj X)
            ((commShiftIso F (-1)).symm.app X.obj₃) (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj X).obj₂)
            (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (invRotate C ⋙ F.mapTriangle).map f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} E
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
inst✝⁸ : HasShift E ℤ
F : C ⥤ D
inst✝⁷ : F.CommShift ℤ
G : D ⥤ E
inst✝⁶ : G.CommShift ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : F.Additive
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    F₁.mapTriangle.map f ≫
        ((F₁.mapTriangle.obj Y).isoMk (F₂.mapTriangle.obj Y) (e.app Y.obj₁) (e.app Y.obj₂) (e.app Y.obj₃) ⋯ ⋯ ⋯).hom =
      ((F₁.mapTriangle.obj X).isoMk (F₂.mapTriangle.obj X) (e.app X.obj₁) (e.app X.obj₂) (e.app X.obj₃) ⋯ ⋯ ⋯).hom ≫
        F₂.mapTriangle.map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ -S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) +
      S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) =
    0

Tactic:
neg_add_cancel

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.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 ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : C ⥤ D
inst✝¹ : F.CommShift ℤ
inst✝ : F.IsTriangulated
⊢ F.map h.m₁ ≫
      F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫ (Functor.commShiftIso F 1).hom.app (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁ =
    F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫ (Functor.commShiftIso F 1).hom.app (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁

Tactic:
simpa using F.congr_map h.comm₂ =≫ (F.commShiftIso 1).hom.app X₁

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
⊢ T₁ ≅ T₂

Tactic:
have h := exists_iso_of_arrow_iso _ _ (inv_rot_of_distTriang _ hT₁)
    (inv_rot_of_distTriang _ hT₂)
    (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ (by
      have := (shiftFunctorCompIsoId C (1 : ℤ) (-1) (by simp)).hom.naturality e₁.hom
      dsimp at this ⊢
      simp only [comp_neg, neg_comp, assoc, neg_inj, ← Functor.map_comp_assoc, ← comm]
      simp [this]))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
⊢ T₁ ≅ T₂
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
a : Paths V
⊢ ∀ {b : Paths V} (f : a ⟶ b), P f

Tactic:
b

Goal state after:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
a b : Paths V
⊢ ∀ (f : a ⟶ b), P f
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ : W.Q ⋙ F ⟶ W.Q ⋙ G
⊢ W.Q.whiskerLeft (natTransExtension τ) = τ

Tactic:
by cat_disch

Goal state after: