mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (triangleh φ₁).mor₂ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b ≫ (triangleh φ₂).mor₂

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₁) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₂)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (triangleh φ₁).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ (triangleh φ₂).mor₃

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₁) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₂).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₂ ≫ map φ₁ φ₂ a b comm = b ≫ (triangle φ₂).mor₂

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ inr φ₁ ≫ map φ₁ φ₂ a b comm = b ≫ inr φ₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangleh φ).rotate.mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (triangleh φ).rotate.obj₁).hom =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).symm.app K ≪≫
          HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ)).hom ≫
      (triangleh (inr φ)).mor₃

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (-(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ)) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)) =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle (inr φ)).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 ((snd φ).shift n) +
          (↑(n.negOnePow • (fst φ).shift n)).comp
            (Cochain.ofHom ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)) ⋯).v
      p q hpq =
    Cochain.v 0 p q hpq

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 ((snd φ).shift n)).v p q hpq +
      ((n.negOnePow • (↑(fst φ)).shift n).comp
            (Cochain.ofHom ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)) ⋯).v
        p q hpq =
    0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (δ (-1) 0 (n.negOnePow • (inl φ).shift n)).v p p ⋯ =
    (Cochain.ofHom
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))).v
      p p ⋯

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (δ (-1) 0 (n.negOnePow • (inl φ).shift n)).v p p ⋯ =
    (Cochain.ofHom
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))).v
      p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ δ (-1) 0 (n.negOnePow • (inl φ).shift n) =
    Cochain.ofHom
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
        (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))

Tactic:
ext p
    dsimp
    simp only [Int.reduceNeg, δ_units_smul, Cochain.δ_shift, δ_inl, Cochain.ofHom_comp, smul_smul,
      Int.units_mul_self, one_smul, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, shiftFunctor_obj_X', shiftFunctor_map_f']

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

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n) ((snd φ).shift n)
            ⋯ ≫
          desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯).f
      p =
    (𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))).f p

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n) ((snd φ).shift n)
            ⋯).f
        p ≫
      (desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯).f
        p =
    𝟙 ((mappingCone φ).X (p + n))
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯ ≫
          lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n)
            ((snd φ).shift n) ⋯).f
      p =
    (𝟙 (mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ))).f p

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯).f
        p ≫
      (lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n)
            ((snd φ).shift n) ⋯).f
        p =
    𝟙 ((mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).X p)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₁ ≫
      (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom =
    (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₁

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) ≫
      (n.negOnePow • 𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom).f p =
    ((n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
          (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂).f
      p

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (n.negOnePow • (inr φ).f (p + n)) ≫ (shiftIso φ n).hom.f p =
    (n.negOnePow • 𝟙 (L.X (p + n))) ≫ (inr ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
          (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
            (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom).f
      p =
    ((shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃).f p

Tactic:
dsimp

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (n.negOnePow • (triangle φ).mor₃.f (p + n) ≫ ((shiftFunctorComm (CochainComplex C ℤ) 1 n).hom.app K).f p) ≫
      𝟙 (K.X (p + 1 + n)) =
    (shiftIso φ n).hom.f p ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃.f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₁ ≫
      (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₁

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ ≫ 𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) =
    𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) ≫ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₂ ≫
      (mapHomologicalComplexIso φ G).hom =
    (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₂).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₂

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ G).hom =
    𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) ≫ inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (Iso.refl ((G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ)).obj₁).hom =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Tactic:
dsimp

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
        (Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app K) ≫
      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) 1).map
        (𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)) =
    (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
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)))
⊢ (contractibleTriangle { as := X }).mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (Iso.refl (contractibleTriangle { as := X }).obj₁).hom =
    h.isoZero.symm.hom ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₃

Tactic:
dsimp

Goal state after:
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
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.mk (F.map X✝.mor₁) (F.map X✝.mor₂) (F.map X✝.mor₃ ≫ (commShiftIso F 1).hom.app X✝.obj₁)).mor₁ ≫
      F.map f.hom₂ =
    F.map f.hom₁ ≫
      (Triangle.mk (F.map Y✝.mor₁) (F.map Y✝.mor₂) (F.map Y✝.mor₃ ≫ (commShiftIso F 1).hom.app Y✝.obj₁)).mor₁

Tactic:
dsimp

Goal state after:
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ F.map X✝.mor₁ ≫ F.map f.hom₂ = F.map f.hom₁ ≫ F.map Y✝.mor₁
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.mk (F.map X✝.mor₁) (F.map X✝.mor₂) (F.map X✝.mor₃ ≫ (commShiftIso F 1).hom.app X✝.obj₁)).mor₂ ≫
      F.map f.hom₃ =
    F.map f.hom₂ ≫
      (Triangle.mk (F.map Y✝.mor₁) (F.map Y✝.mor₂) (F.map Y✝.mor₃ ≫ (commShiftIso F 1).hom.app Y✝.obj₁)).mor₂

Tactic:
dsimp

Goal state after:
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ F.map X✝.mor₂ ≫ F.map f.hom₃ = F.map f.hom₂ ≫ F.map Y✝.mor₂