awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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))
⊢ 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))
have 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₂.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 [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
      mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by lia),
      cocycleOfDegreewiseSplit, r_f, Int.reduceNeg, Cochain.ofHom_v, sub_comp, assoc,
      Hom.comm, comp_sub, mappingCone.inl_v_fst_v_assoc, mappingCone.inl_v_snd_v_assoc,
      shiftFunctor_obj_X', zero_comp, sub_zero, homOfDegreewiseSplit_f,
      mappingCone.inr_f_fst_v_assoc, comp_zero, zero_sub, mappingCone.inr_f_snd_v_assoc,
      neg_neg, mappingCone.inr_f_d_assoc, shiftFunctor_obj_d',
      Int.negOnePow_one, neg_comp, sub_neg_eq_add, zero_add, and_true,
      Units.neg_smul, one_smul, comp_neg, ShortComplex.map_X₂, eval_obj, Cocycle.mk_coe,
      Cochain.mk_v]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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₂.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)))
have 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)))
Tactic: simp only [← S.g.comm_assoc, reassoc_of% s_g, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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 σ))
    (-mappingCone.inr (homOfDegreewiseSplit S σ) :
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁ ⟶
        mappingCone (homOfDegreewiseSplit S σ))
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
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 : ℤ
⊢ 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)
have h : 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
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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))
⊢ 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)
have 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 sorry)
      (ShortComplex.Splitting.r (σ (n + 1)) ≫
        𝟙 (S.X₁.X (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: dsimp [mappingConeHomOfDegreewiseSplitXIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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))
⊢ 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
have 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 sorry)
      (ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ 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
have h₂ : HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n sorry)
    (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₂ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ 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
have h₃ : HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    ((S.f ≫ S.g).f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n sorry)
    (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₂ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₃ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      ((S.f ≫ S.g).f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ 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
have h₄ : HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (Hom.f 0 (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n sorry)
    (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₂ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₃ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      ((S.f ≫ S.g).f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₄ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (Hom.f 0 (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ 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
have h₅ : HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
    (0 ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n sorry)
    (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₂ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (S.f.f (n + 1) ≫ S.g.f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₃ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      ((S.f ≫ S.g).f (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₄ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (Hom.f 0 (n + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
h₅ :
  HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n)
      (0 ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (n + 1) n ⋯)
      (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
    -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
⊢ 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
have h₆ : HSub.hSub (α := S.X₁.X (n + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X n) 0
    (S.f.f (n + 1) ≫ ShortComplex.Splitting.r (σ (n + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n) =
  -Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) n
Tactic: rw [id_comp, comp_sub, ← comp_f_assoc, S.zero, zero_f, zero_comp, zero_sub, reassoc_of% h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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
⊢ Iso.inv (mappingConeHomOfDegreewiseSplitIso S σ) ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ =
    -CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.g
have 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
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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 : ℤ
⊢ (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
have 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 sorry)
      (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: dsimp [mappingConeHomOfDegreewiseSplitXIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
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
⊢ (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₁
have dsimp : homOfDegreewiseSplit S σ ≫
    𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) S.X₁) =
  𝟙 S.X₃ ≫ homOfDegreewiseSplit S σ
Tactic: dsimp