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))
p : ℤ
this : Mono (X := S.X₁.X (p + 2)) (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ p + 1 = p + 2 - 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))
p : ℤ
this : Mono (X := S.X₁.X (p + 2)) (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ p + 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))
p : ℤ
this : Mono (X := S.X₁.X (p + 2)) (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ Int.negOnePow 2 = 1

Tactic:
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))
n : ℤ
⊢ (homOfDegreewiseSplit S σ).f n = (↑(cocycleOfDegreewiseSplit S σ) : Cochain S.X₃ S.X₁ 1).v n (n + 1) ⋯

Tactic:
simp [homOfDegreewiseSplit, Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl]

Premises used: CochainComplex.homOfDegreewiseSplit, CochainComplex.HomComplex.Cochain.rightShift_v, 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
p q : ℤ
hpq : p + 1 = q
⊢ p + 1 + 0 = q

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 q : ℤ
hpq : p + 1 = q
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁).X p ⟶
    ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) q))

Tactic:
exact (Cochain.ofHom S.f).v (p + 1) q (by lia)

Premises used: CochainComplex.HomComplex.Cochain.ofHom, HAdd.hAdd, CochainComplex.HomComplex.Cochain.v, CategoryTheory.ShortComplex.f, OfNat.ofNat
-- 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 q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

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 q : ℤ
hpq : p + 1 = q
⊢ S.X₂.X q ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p

Tactic:
exact (σ q).r ≫ (S.X₁.XIsoOfEq hpq.symm).hom ≫
      (mappingCone.inr (homOfDegreewiseSplit S σ)).f p

Premises used: HomologicalComplex.Hom.f, CochainComplex.mappingCone.inr, CategoryTheory.ShortComplex.X₁, HomologicalComplex.XIsoOfEq, CochainComplex.homOfDegreewiseSplit, CategoryTheory.ShortComplex.Splitting.r, Eq.symm, CategoryTheory.Iso.hom
-- 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 q : ℤ
hpq : p + 1 = q
subst :
  HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
⊢ HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) q)))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            q hpq ≫
          (σ q).s)
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) q ⋯) ≫
      HSub.hSub (α := S.X₂.X q ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f q ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) q p ⋯)
        ((σ q).r ≫ (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)

Tactic:
subst hpq
-- 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 : ℤ
⊢ 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))))

Tactic:
have s_g := (σ (p + 1)).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 : ℤ
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))))
⊢ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ≫ ShortComplex.Splitting.r (σ (p + 1)) =
    𝟙 (ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))

Tactic:
have f_r := (σ (p + 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
p : ℤ
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))))
f_r :
  ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ≫ ShortComplex.Splitting.r (σ (p + 1)) =
    𝟙 (ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
dsimp :
  HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          𝟙 (S.X₁.X (p + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
⊢ HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)

Tactic:
dsimp at s_g 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
p : ℤ
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
f_r : S.f.f (p + 1) ≫ ShortComplex.Splitting.r (σ (p + 1)) = 𝟙 (S.X₁.X (p + 1))
simp :
  Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
    (S.f.f (p + 1) ≫ S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯) 0
⊢ HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          𝟙 (S.X₁.X (p + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)

Tactic:
simp only [Cochain.ofHom_v, Int.reduceNeg, id_comp, comp_sub, sub_comp, assoc,
        reassoc_of% s_g, ShortComplex.Splitting.s_r_assoc, ShortComplex.map_X₃, eval_obj,
        ShortComplex.map_X₁, zero_comp, comp_zero, reassoc_of% f_r, zero_sub, sub_neg_eq_add,
        mappingCone.ext_from_iff _ (p + 1) _ rfl, comp_add, mappingCone.inl_v_fst_v_assoc,
        mappingCone.inl_v_snd_v_assoc, shiftFunctor_obj_X', sub_zero, add_zero, comp_id,
        mappingCone.inr_f_fst_v_assoc, mappingCone.inr_f_snd_v_assoc, add_eq_right, neg_eq_zero,
        true_and]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.map_X₃, sub_zero, Int.reduceNeg, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.map_X₁, CochainComplex.mappingCone.ext_from_iff, neg_eq_zero, CochainComplex.HomComplex.Cochain.ofHom_v, CategoryTheory.Category.comp_id, HomologicalComplex.eval_obj, CochainComplex.mappingCone.inl_v_snd_v_assoc, CochainComplex.mappingCone.inr_f_fst_v_assoc, HAdd.hAdd, add_eq_right, CategoryTheory.Preadditive.comp_add, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Limits.zero_comp, add_zero, OfNat.ofNat, CategoryTheory.Preadditive.comp_sub, CochainComplex.mappingCone.inl_v_fst_v_assoc, sub_neg_eq_add, CategoryTheory.Preadditive.sub_comp, rfl, true_and, zero_sub, CategoryTheory.Category.id_comp, CategoryTheory.ShortComplex.Splitting.s_r_assoc
-- 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 : ℤ
s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
f_r : S.f.f (p + 1) ≫ ShortComplex.Splitting.r (σ (p + 1)) = 𝟙 (S.X₁.X (p + 1))
rw :
  Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
    ((S.f ≫ S.g).f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯) 0
rw₁ :
  Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
    (Hom.f 0 (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯) 0
rw₂ :
  Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
    (0 ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯) 0
rw₃ rw₄ : Eq.{v + 1} (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p) 0 0
⊢ Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
    (S.f.f (p + 1) ≫ S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯) 0

Tactic:
rw [← comp_f_assoc, S.zero, zero_f, zero_comp]

Premises used: HomologicalComplex.zero_f, CategoryTheory.ShortComplex.zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.comp_f_assoc
-- 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 q : ℤ
hpq : p + 1 = q
subst :
  HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) ≫
      HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) =
    𝟙 (S.X₂.X (p + 1))
⊢ HSub.hSub (α := S.X₂.X q ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f q ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) q p ⋯)
        ((σ q).r ≫ (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) ≫
      HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) q)))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            q hpq ≫
          (σ q).s)
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) q ⋯) =
    𝟙 (S.X₂.X q)

Tactic:
subst hpq
-- 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 : ℤ
⊢ HAdd.hAdd (α :=
      ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ⟶
        ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
      (ShortComplex.Splitting.r (σ (p + 1)) ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
      (ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ≫ ShortComplex.Splitting.s (σ (p + 1))) =
    𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))

Tactic:
have h := (σ (p + 1)).id
-- 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 : ℤ
h :
  HAdd.hAdd (α :=
      ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ⟶
        ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
      (ShortComplex.Splitting.r (σ (p + 1)) ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
      (ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ≫ ShortComplex.Splitting.s (σ (p + 1))) =
    𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
dsimp :
  HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          𝟙 (S.X₁.X (p + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) ≫
      HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) =
    𝟙 (S.X₂.X (p + 1))
⊢ HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) ≫
      HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) =
    𝟙 (S.X₂.X (p + 1))

Tactic:
dsimp at h ⊢
-- 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 : ℤ
h :
  HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1))
      (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 1))) =
    𝟙 (S.X₂.X (p + 1))
simp :
  HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 1)))
      (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1)) =
    HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1))
      (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 1)))
⊢ HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          𝟙 (S.X₁.X (p + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) ≫
      HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) =
    𝟙 (S.X₂.X (p + 1))

Tactic:
simp only [id_comp, Cochain.ofHom_v, comp_sub, sub_comp, assoc, mappingCone.inl_v_fst_v_assoc,
      mappingCone.inr_f_fst_v_assoc, shiftFunctor_obj_X', zero_comp, comp_zero, sub_zero,
      mappingCone.inl_v_snd_v_assoc, mappingCone.inr_f_snd_v_assoc, zero_sub, sub_neg_eq_add, ← h]

Premises used: CategoryTheory.Category.assoc, sub_zero, CategoryTheory.Limits.comp_zero, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.mappingCone.inl_v_snd_v_assoc, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.comp_sub, CochainComplex.mappingCone.inl_v_fst_v_assoc, sub_neg_eq_add, CategoryTheory.Preadditive.sub_comp, zero_sub, 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
p : ℤ
h :
  HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1))
      (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 1))) =
    𝟙 (S.X₂.X (p + 1))
⊢ HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 1)))
      (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1)) =
    HAdd.hAdd (α := S.X₂.X (p + 1) ⟶ S.X₂.X (p + 1)) (ShortComplex.Splitting.r (σ (p + 1)) ≫ S.f.f (p + 1))
      (S.g.f (p + 1) ≫ ShortComplex.Splitting.s (σ (p + 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
p : ℤ
⊢ 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))

Tactic:
have r_f := (σ (p + 1 + 1)).r_f
-- 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))
⊢ 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))))

Tactic:
have s_g := (σ (p + 1)).s_g