mathlib-initiative/mathlib-tactics huggingface dataset:
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 c : ℤ
T : Triangle C
⊢ (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
      (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T) =
    eqToHom ⋯ ≫
      (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
        (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ ((shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T)).hom₁ =
    (eqToHom ⋯ ≫
        (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
          (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)).hom₁

case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ ((shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T)).hom₂ =
    (eqToHom ⋯ ≫
        (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
          (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)).hom₂

case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ ((shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T)).hom₃ =
    (eqToHom ⋯ ≫
        (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
          (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)).hom₃
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
⊢ T.mor₃ = 0 ↔ Epi T.mor₂

Tactic:
constructor

Goal state after:
case mp
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
⊢ T.mor₃ = 0 → Epi T.mor₂

case mpr
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
⊢ Epi T.mor₂ → T.mor₃ = 0
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
⊢ T.mor₁ = 0 ↔ Mono T.mor₂

Tactic:
constructor

Goal state after:
case mp
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
⊢ T.mor₁ = 0 → Mono T.mor₂

case mpr
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
⊢ Mono T.mor₂ → T.mor₁ = 0
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
⊢ IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
constructor

Goal state after:
case mp
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
⊢ IsZero T.obj₂ → T.mor₁ = 0 ∧ T.mor₂ = 0

case mpr
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
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0 → IsZero T.obj₂
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
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂

Tactic:
constructor

Goal state after:
case mp
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
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 → IsIso T.mor₂

case mpr
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
⊢ IsIso T.mor₂ → T.mor₁ = 0 ∧ T.mor₃ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mpr
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
a✝ : IsIso T.mor₂
⊢ Mono T.mor₂ ∧ Epi T.mor₂

Tactic:
constructor

Goal state after:
case mpr.left
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
a✝ : IsIso T.mor₂
⊢ Mono T.mor₂

case mpr.right
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
a✝ : IsIso T.mor₂
⊢ Epi T.mor₂
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom = biprod.inl

Tactic:
ext

Goal state after:
case h₀
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.fst = biprod.inl ≫ biprod.fst

case h₁
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.snd = biprod.inl ≫ biprod.snd
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ inr φ ≫ (triangle φ).mor₃ = 0

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ ≫ (triangle φ).mor₃).f i✝ = HomologicalComplex.Hom.f 0 i✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ 0 ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map (𝟙 { as := X }) =
    h.isoZero.inv ≫
      (quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle (𝟙 X)).mor₃ ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X

Tactic:
ext

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C → T.rotate ∈ distinguishedTriangles C

case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T.rotate ∈ distinguishedTriangles C → T ∈ distinguishedTriangles C
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.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
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.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f.hom₁ = g.hom₁

case h₂
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.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f.hom₂ = g.hom₂

case h₃
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.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f.hom₃ = g.hom₃
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 ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
⊢ F.mapTriangleCommShiftIso (n + m) = CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)

Tactic:
ext

Goal state after:
case h₁
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✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₁ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₁

case h₂
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✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₂ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₂

case h₃
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✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
x✝ : Triangle C
⊢ ((F.mapTriangleCommShiftIso (n + m)).hom.app x✝).hom₃ =
    ((CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)).hom.app x✝).hom₃
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
⊢ F.map (prod.lift (𝟙 X₁) 0) ≫ prodComparison F X₁ X₃ = 𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0

Tactic:
ext

Goal state after:
case h₁
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
⊢ (F.map (prod.lift (𝟙 X₁) 0) ≫ prodComparison F X₁ X₃) ≫ prod.fst =
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0) ≫ prod.fst

case h₂
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ X₃ : C
⊢ (F.map (prod.lift (𝟙 X₁) 0) ≫ prodComparison F X₁ X₃) ≫ prod.snd =
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0) ≫ prod.snd
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
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₁.IsTriangulated ↔ F₂.IsTriangulated

Tactic:
constructor

Goal state after:
case mp
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
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₁.IsTriangulated → F₂.IsTriangulated

case mpr
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
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₂.IsTriangulated → F₁.IsTriangulated
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 (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ = F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁

Tactic:
dsimp; rw [← F.map_comp, comm]

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
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (Iso.refl (triangle φ).rotate.obj₁).hom =
    (Iso.refl (triangle φ).rotate.obj₃).hom ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃

Tactic:
ext

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
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ ((triangle φ).rotate.mor₃ ≫
          (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (Iso.refl (triangle φ).rotate.obj₁).hom).f
      i✝ =
    ((Iso.refl (triangle φ).rotate.obj₃).hom ≫
          (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃).f
      i✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles ↔ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles → ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ (∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) → T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j

Tactic:
simp [opcyclesToCycles]

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

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

Tactic:
ext

Goal state after:
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

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

Tactic:
constructor

Goal state after:
case mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

case mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
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)
⊢ P = ⊤

Tactic:
ext

Goal state after:
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
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)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝