awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))) =
    𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1)))) -
      ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g :
  ShortComplex.Splitting.s (σ (p + 1)) ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1))) =
    𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
dsimp :
  Eq (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
    (Iso.hom (mappingConeHomOfDegreewiseSplitXIso S σ p (p + 1) ⋯) ≫
        HSMul.hSMul (α := ℤˣ) (β := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1 + 1)) (-1) (S.X₂.d (p + 1) (p + 1 + 1)) :
      (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
    ((mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫
        Iso.hom (mappingConeHomOfDegreewiseSplitXIso S σ (p + 1) (p + 1 + 1) ⋯) :
      (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
⊢ Eq (α :=
    (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₂).X (p + 1))
    (Iso.hom
        ((fun (p : ℤ) ↦
            (mappingConeHomOfDegreewiseSplitXIso S σ p (p + Discrete.as { as := 1 }) ⋯ :
              (mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X (p + Discrete.as { as := 1 })))
          p) ≫
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₂).d p (p + 1))
    (CategoryStruct.comp (Y := (mappingCone (homOfDegreewiseSplit S σ)).X (p + 1))
      ((mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1))
      (Iso.hom
        ((fun (p : ℤ) ↦
            (mappingConeHomOfDegreewiseSplitXIso S σ p (p + Discrete.as { as := 1 }) ⋯ :
              (mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X (p + Discrete.as { as := 1 })))
          (p + 1))))

Tactic:
dsimp at r_f s_g ⊢
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ S.f.f (p + 1 + 1) =
    𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
linarith : p + 1 + -1 < p → -1 + (p + 1 + -1 + 1 - p) = 0
linarith₁ : p < p + 1 + -1 → -1 + (p + 1 - (p + 1 + -1)) = 0
⊢ p + 1 + -1 = p

Tactic:
linarith
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ S.f.f (p + 1 + 1) =
    𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
⊢ p + 1 + 1 + -1 = p + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ S.f.f (p + 1 + 1) =
    𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
simp :
  -ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) =
    -S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)) -
      HSub.hSub (α := S.X₃.X (p + 1) ⟶ S.X₂.X (p + 1 + 1))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1))
        (S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)))
⊢ -ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) =
    -S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)) -
      HSub.hSub (α := S.X₃.X (p + 1) ⟶ S.X₂.X (p + 1 + 1))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) ≫ 𝟙 (S.X₂.X (p + 1 + 1)))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫
          S.X₂.d (p + 1) (p + 1 + 1) ≫ S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)))

Tactic:
simp only [← S.g.comm_assoc, reassoc_of% s_g, comp_id]

Premises used: CategoryTheory.Category.comp_id, HomologicalComplex.Hom.comm_assoc, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
r_f :
  ShortComplex.Splitting.r (σ (p + 1 + 1)) ≫ S.f.f (p + 1 + 1) =
    𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1))
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
⊢ -ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1) =
    -S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)) -
      HSub.hSub (α := S.X₃.X (p + 1) ⟶ S.X₂.X (p + 1 + 1))
        (ShortComplex.Splitting.s (σ (p + 1)) ≫ S.X₂.d (p + 1) (p + 1 + 1))
        (S.X₃.d (p + 1) (p + 1 + 1) ≫ ShortComplex.Splitting.s (σ (p + 1 + 1)))

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
h :
  ∀ (n : ℤ),
    Eq (α :=
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
        (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (Hom.f
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f ≫
            Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ))
          n :
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
          (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (Hom.f (-mappingCone.inr (homOfDegreewiseSplit S σ)) n :
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
          (mappingCone (homOfDegreewiseSplit S σ)).X n)
⊢ Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
      mappingCone (homOfDegreewiseSplit S σ))
    (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f ≫
        Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))
    (-mappingCone.inr (homOfDegreewiseSplit S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
n : ℤ
⊢ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (n + 1))) ≫ ShortComplex.Splitting.r (σ (n + 1)) =
    𝟙 (ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (n + 1))))

Tactic:
have h := (σ (n + 1)).f_r
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
n : ℤ
h : S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) = 𝟙 (S.X₁.X (n + 1))
h₁ :
  S.f.f (n + 1) ≫
      HSub.hSub (α := S.X₂.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
        (S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
        (ShortComplex.Splitting.r (σ (n + 1)) ≫
          𝟙 (S.X₁.X (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
      (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (Hom.f
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f ≫
          Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ))
        n :
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
        (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (Hom.f (-mappingCone.inr (homOfDegreewiseSplit S σ)) n :
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X n ⟶
        (mappingCone (homOfDegreewiseSplit S σ)).X n)

Tactic:
dsimp [mappingConeHomOfDegreewiseSplitXIso]

Premises used: CochainComplex.mappingConeHomOfDegreewiseSplitXIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
h :
  ∀ (n : ℤ),
    (Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃).f n =
      Hom.f (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g)
        n
⊢ Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ =
    -CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
n : ℤ
h :
  HSub.hSub (α := S.X₂.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
        (S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
        (ShortComplex.Splitting.r (σ (n + 1)) ≫
          𝟙 (S.X₁.X (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃.f n =
    -S.g.f (n + 1)
⊢ (Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃).f n =
    Hom.f (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g) n

Tactic:
dsimp [mappingConeHomOfDegreewiseSplitXIso]

Premises used: CochainComplex.mappingConeHomOfDegreewiseSplitXIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
n : ℤ
⊢ HSub.hSub (α := S.X₂.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
        (S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
        (ShortComplex.Splitting.r (σ (n + 1)) ≫
          𝟙 (S.X₁.X (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃.f n =
    -S.g.f (n + 1)

Tactic:
simp only [Int.reduceNeg, id_comp, sub_comp, assoc, mappingCone.inl_v_triangle_mor₃_f,
    shiftFunctor_obj_X, shiftFunctorObjXIso, XIsoOfEq_rfl, Iso.refl_inv, comp_neg, comp_id,
    mappingCone.inr_f_triangle_mor₃_f, comp_zero, sub_zero]

Premises used: CategoryTheory.Category.assoc, sub_zero, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CategoryTheory.Iso.refl_inv, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
dsimp :
  homOfDegreewiseSplit S σ ≫
      𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) =
    𝟙 S.X₃ ≫ homOfDegreewiseSplit S σ
⊢ (triangleOfDegreewiseSplit S σ).rotate.rotate.mor₁ ≫
      Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₂) =
    Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₁) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₁

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
⊢ homOfDegreewiseSplit S σ ≫
      𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) =
    𝟙 S.X₃ ≫ homOfDegreewiseSplit S σ

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
dsimp :
  Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
      mappingCone (homOfDegreewiseSplit S σ))
    ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f) ≫
        Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))
    (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) ≫
        mappingCone.inr (homOfDegreewiseSplit S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))
⊢ (triangleOfDegreewiseSplit S σ).rotate.rotate.mor₂ ≫ Iso.hom (Iso.symm (mappingConeHomOfDegreewiseSplitIso S σ)) =
    Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₂) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
⊢ Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
      mappingCone (homOfDegreewiseSplit S σ))
    ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.f) ≫
        Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))
    (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) ≫
        mappingCone.inr (homOfDegreewiseSplit S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))

Tactic:
simp only [neg_comp, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv,
      neg_neg, id_comp]

Premises used: CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, neg_neg, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
dsimp :
  (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g) ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 S.X₃) =
    Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃
⊢ (triangleOfDegreewiseSplit S σ).rotate.rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangleOfDegreewiseSplit S σ).rotate.rotate.obj₁)) =
    Iso.hom (Iso.symm (mappingConeHomOfDegreewiseSplitIso S σ)) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
⊢ (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g) ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 S.X₃) =
    Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃

Tactic:
simp only [CategoryTheory.Functor.map_id, comp_id,
      mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₁ ≫ (triangle φ).rotate.mor₂ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ HAdd.hAdd (α :=
      ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)) ⟶
        ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)))
      (β :=
      ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)) ⟶
        ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)))
      (Cochain.v (snd φ) n n ⋯ ≫ ShortComplex.f ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)) :
        ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)) ⟶
          ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)))
      (ShortComplex.g ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)) ≫
        (-Cochain.v (inl φ) (n + 1) n ⋯)) =
    𝟙 (ShortComplex.X₂ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)))

Tactic:
simp [ext_from_iff φ _ _ rfl]

Premises used: CochainComplex.mappingCone.ext_from_iff, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
⊢ (↑(cocycleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)) :
          Cochain (triangleRotateShortComplex φ).X₃ (triangleRotateShortComplex φ).X₁ 1).v
      p (p + 1) ⋯ =
    -φ.f (p + Discrete.as { as := 1 })

Tactic:
simp [cocycleOfDegreewiseSplit, d_snd_v φ p (p + 1) rfl]

Premises used: CochainComplex.cocycleOfDegreewiseSplit, CochainComplex.mappingCone.d_snd_v, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₁ ≫ Iso.hom (Iso.refl (triangle φ).rotate.obj₂) =
    Iso.hom (Iso.refl (triangle φ).rotate.obj₁) ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₁

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
K L : CochainComplex.{v, u_1, 0} C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₂ ≫ Iso.hom (Iso.refl (triangle φ).rotate.obj₃) =
    Iso.hom (Iso.refl (triangle φ).rotate.obj₂) ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₂

Tactic:
simp