awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
refine_1 : T₁.mor₂ ≫ γ.hom₃ = b ≫ T₂.mor₂
refine_2 :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) a =
    γ.hom₃ ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

Tactic:
refine ⟨γ.hom₃, ?_, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
⊢ T₁.mor₂ ≫ γ.hom₃ = b ≫ T₂.mor₂

Tactic:
simpa only [triangleCategory_comp, Functor.mapTriangle_obj, triangle_obj₁, triangle_obj₂,
      triangle_obj₃, triangle_mor₁, triangle_mor₂, TriangleMorphism.comp_hom₃, Triangle.mk_obj₃,
      trianglehMapOfHomotopy_hom₃, TriangleMorphism.comm₂_assoc, Triangle.mk_obj₂,
      Triangle.mk_mor₂, assoc, Iso.hom_inv_id_triangle_hom₂, comp_id,
      Iso.hom_inv_id_triangle_hom₂_assoc, γ] using comm₂

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.triangle_mor₁, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Iso.hom_inv_id_triangle_hom₂, CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Pretriangulated.Triangle.mk_mor₂, CochainComplex.mappingCone.triangle_mor₂, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CategoryTheory.Pretriangulated.triangleCategory_comp, CategoryTheory.Pretriangulated.Triangle.mk_obj₂, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc, CochainComplex.mappingCone.triangle_obj₂, CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃, CategoryTheory.Pretriangulated.Triangle.mk_obj₃, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.mappingCone.triangle_obj₃
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
⊢ T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) a =
    γ.hom₃ ≫ T₂.mor₃

Tactic:
simpa only [triangleCategory_comp, Functor.mapTriangle_obj, triangle_obj₁, triangle_obj₂,
      triangle_obj₃, triangle_mor₁, triangle_mor₂, TriangleMorphism.comp_hom₃, Triangle.mk_obj₃,
      trianglehMapOfHomotopy_hom₃, assoc, Triangle.mk_obj₁, Iso.hom_inv_id_triangle_hom₁, comp_id,
      Iso.hom_inv_id_triangle_hom₁_assoc, γ] using comm₃

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.triangle_mor₁, CategoryTheory.Functor.mapTriangle_obj, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.triangle_mor₂, CategoryTheory.Iso.hom_inv_id_triangle_hom₁, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CategoryTheory.Pretriangulated.triangleCategory_comp, CochainComplex.mappingCone.triangle_obj₂, CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃, CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc, CategoryTheory.Pretriangulated.Triangle.mk_obj₃, CategoryTheory.Pretriangulated.Triangle.mk_obj₁, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.mappingCone.triangle_obj₃
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (CochainComplex.mappingCone.triangleh f)

Tactic:
⟨_, _, f, ⟨Iso.refl _⟩⟩

Premises used: Set.Mem, setOf, CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K_1 L_1 : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K_1 ⟶ L_1
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_8 : G.Additive
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh f
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_2, u_2, 0} D (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive D (ComplexShape.up ℤ)) ⋯ _)
    (Functor.obj (Functor.mapTriangle (G.mapHomotopyCategory (ComplexShape.up ℤ))) T)

Tactic:
⟨_, _, _, ⟨(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.mapIso e ≪≫
      CochainComplex.mappingCone.mapTrianglehIso f G⟩⟩

Premises used: Set.Mem, setOf, Int, Nonempty.intro, CategoryTheory.Functor.mapTriangle, CategoryTheory.Functor.mapHomotopyCategory, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Functor.mapIso, CochainComplex.mappingCone.mapTrianglehIso, ComplexShape.up, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K_1 L_1 : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K_1 ⟶ L_1
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_8 : G.Additive
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh f
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_2, u_2, 0} D (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive D (ComplexShape.up ℤ)) ⋯ _)
    (Functor.obj (Functor.mapTriangle (G.mapHomotopyCategory (ComplexShape.up ℤ))) T)

Tactic:
exact ⟨_, _, _, ⟨(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.mapIso e ≪≫
      CochainComplex.mappingCone.mapTrianglehIso f G⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
a : ¬(ComplexShape.up ℤ).Rel (i + n) (j + n)
⊢ HSMul.hSMul (β := K.X (i + n) ⟶ K.X (j + n)) n.negOnePow (K.d (i + n) (j + n)) = 0

Tactic:
rw [K.shape, smul_zero]

Premises used: smul_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
hij' : (ComplexShape.up ℤ).Rel (i + n) (j + n)
a : (ComplexShape.up ℤ).Rel i j
⊢ False

Tactic:
apply hij
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
hij' : i + n + 1 = j + n
⊢ i + 1 = j

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j k : ℤ
h : (ComplexShape.up ℤ).Rel i j
h_1 : (ComplexShape.up ℤ).Rel j k
⊢ HSMul.hSMul (β := K.X (i + n) ⟶ K.X (j + n)) n.negOnePow (K.d (i + n) (j + n)) ≫
      HSMul.hSMul (β := K.X (j + n) ⟶ K.X (k + n)) n.negOnePow (K.d (j + n) (k + n)) =
    0

Tactic:
simp only [Linear.comp_units_smul, Linear.units_smul_comp, d_comp_d, smul_zero]

Premises used: CategoryTheory.Linear.units_smul_comp, smul_zero, CategoryTheory.Linear.comp_units_smul, HomologicalComplex.d_comp_d
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
X Y : CochainComplex.{v, u, 0} C ℤ
φ : X ⟶ Y
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
dsimp :
  φ.f (i + n) ≫ HSMul.hSMul (β := Y.X (i + n) ⟶ Y.X (j + n)) n.negOnePow (Y.d (i + n) (j + n)) =
    HSMul.hSMul (β := X.X (i + n) ⟶ X.X (j + n)) n.negOnePow (X.d (i + n) (j + n)) ≫ φ.f (j + n)
⊢ φ.f (i + n) ≫
      { X := fun (i : ℤ) ↦ Y.X (i + n),
            d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := Y.X (x + n) ⟶ Y.X (x_1 + n)) n.negOnePow (Y.d (x + n) (x_1 + n)),
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }.d
        i j =
    { X := fun (i : ℤ) ↦ X.X (i + n),
            d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := X.X (x + n) ⟶ X.X (x_1 + n)) n.negOnePow (X.d (x + n) (x_1 + n)),
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }.d
        i j ≫
      φ.f (j + n)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
X Y : CochainComplex.{v, u, 0} C ℤ
φ : X ⟶ Y
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
⊢ φ.f (i + n) ≫ HSMul.hSMul (β := Y.X (i + n) ⟶ Y.X (j + n)) n.negOnePow (Y.d (i + n) (j + n)) =
    HSMul.hSMul (β := X.X (i + n) ⟶ X.X (j + n)) n.negOnePow (X.d (i + n) (j + n)) ≫ φ.f (j + n)

Tactic:
simp only [Linear.comp_units_smul, Hom.comm, Linear.units_smul_comp]

Premises used: CategoryTheory.Linear.units_smul_comp, CategoryTheory.Linear.comp_units_smul, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
X : CochainComplex.{v, u, 0} C ℤ
⊢ { f := fun (x : ℤ) ↦ Hom.f (𝟙 X) (x + n), comm' := ⋯ } =
    𝟙
      { X := fun (i : ℤ) ↦ X.X (i + n),
        d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := X.X (x + n) ⟶ X.X (x_1 + n)) n.negOnePow (X.d (x + n) (x_1 + n)),
        shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
X Y Z : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    { X := fun (i : ℤ) ↦ X.X (i + n),
        d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := X.X (x + n) ⟶ X.X (x_1 + n)) n.negOnePow (X.d (x + n) (x_1 + n)),
        shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) } ⟶
      { X := fun (i : ℤ) ↦ Z.X (i + n),
        d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := Z.X (x + n) ⟶ Z.X (x_1 + n)) n.negOnePow (Z.d (x + n) (x_1 + n)),
        shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (x : ℤ) ↦ (f ≫ g).f (x + n), comm' := ⋯ }
    (CategoryStruct.comp (Y :=
      { X := fun (i : ℤ) ↦ Y.X (i + n),
        d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := Y.X (x + n) ⟶ Y.X (x_1 + n)) n.negOnePow (Y.d (x + n) (x_1 + n)),
        shape := ⋯, d_comp_d' := ⋯ })
      { f := fun (x : ℤ) ↦ f.f (x + n), comm' := ⋯ } { f := fun (x : ℤ) ↦ g.f (x + n), comm' := ⋯ })

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
h : n = 0
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
⊢ i = i + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
h : n = 0
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h_1 : (ComplexShape.up ℤ).Rel x x_1
⊢ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) x) ≫
      (Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K).d x x_1 =
    (Functor.obj (shiftFunctor C n) K).d x x_1 ≫ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) x_1)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
h : n = 0
X Y : CochainComplex.{v, u, 0} C ℤ
x : X ⟶ Y
h₁ :
  ∀ (i : ℤ),
    Eq (α := (Functor.obj (shiftFunctor C n) X).X i ⟶ (Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) Y).X i)
      (Hom.f
        (CategoryTheory.Functor.map (shiftFunctor C n) x ≫
          Iso.hom
            ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
                (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
                  Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
              Y))
        i)
      (Hom.f
        (Iso.hom
            ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
                (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
                  Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
              X) ≫
          CategoryTheory.Functor.map (𝟭 (CochainComplex.{v, u, 0} C ℤ)) x)
        i)
⊢ Eq (α := Functor.obj (shiftFunctor C n) X ⟶ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) Y)
    (CategoryTheory.Functor.map (shiftFunctor C n) x ≫
      Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
              Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
          Y))
    (Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
              Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (CochainComplex.{v, u, 0} C ℤ)) x)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
h : n = 0
X Y : CochainComplex.{v, u, 0} C ℤ
x : X ⟶ Y
i : ℤ
⊢ Eq (α := (Functor.obj (shiftFunctor C n) X).X i ⟶ (Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) Y).X i)
    (Hom.f
      (CategoryTheory.Functor.map (shiftFunctor C n) x ≫
        Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
                Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
            Y))
      i)
    (Hom.f
      (Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
                Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
            X) ≫
        CategoryTheory.Functor.map (𝟭 (CochainComplex.{v, u, 0} C ℤ)) x)
      i)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
⊢ i + n₂ + n₁ = i + n₁₂

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h_1 : (ComplexShape.up ℤ).Rel x x_1
subst :
  Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x) ≫
      (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
    (Functor.obj (shiftFunctor C (n₁ + n₂)) K).d x x_1 ≫
      Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x_1)
⊢ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) x) ≫
      (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
    (Functor.obj (shiftFunctor C n₁₂) K).d x x_1 ≫
      Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) x_1)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ : ℤ
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h : (ComplexShape.up ℤ).Rel x x_1
dsimp :
  (XIsoOfEq K ⋯).hom ≫
      (n₂.negOnePow •
        HSMul.hSMul (β := K.X (x + n₂ + n₁) ⟶ K.X (x_1 + n₂ + n₁)) n₁.negOnePow (K.d (x + n₂ + n₁) (x_1 + n₂ + n₁))) =
    HSMul.hSMul (β := K.X (x + (n₁ + n₂)) ⟶ K.X (x_1 + (n₁ + n₂))) (n₁ + n₂).negOnePow
        (K.d (x + (n₁ + n₂)) (x_1 + (n₁ + n₂))) ≫
      (XIsoOfEq K ⋯).hom
⊢ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x) ≫
      (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
    (Functor.obj (shiftFunctor C (n₁ + n₂)) K).d x x_1 ≫
      Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x_1)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ : ℤ
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h : (ComplexShape.up ℤ).Rel x x_1
⊢ (XIsoOfEq K ⋯).hom ≫
      (n₂.negOnePow •
        HSMul.hSMul (β := K.X (x + n₂ + n₁) ⟶ K.X (x_1 + n₂ + n₁)) n₁.negOnePow (K.d (x + n₂ + n₁) (x_1 + n₂ + n₁))) =
    HSMul.hSMul (β := K.X (x + (n₁ + n₂)) ⟶ K.X (x_1 + (n₁ + n₂))) (n₁ + n₂).negOnePow
        (K.d (x + (n₁ + n₂)) (x_1 + (n₁ + n₂))) ≫
      (XIsoOfEq K ⋯).hom

Tactic:
simp only [add_comm n₁ n₂, Int.negOnePow_add, Linear.units_smul_comp,
        Linear.comp_units_smul, d_comp_XIsoOfEq_hom, smul_smul, XIsoOfEq_hom_comp_d]

Premises used: CategoryTheory.Linear.units_smul_comp, smul_smul, Int.negOnePow_add, HomologicalComplex.XIsoOfEq_hom_comp_d, CategoryTheory.Linear.comp_units_smul, add_comm, HomologicalComplex.d_comp_XIsoOfEq_hom