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 : ℤ
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))))
⊢ 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)
have 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) sorry ≫
        ShortComplex.Splitting.s (σ (p + 1)))
      (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p sorry ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) sorry) ≫
    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 sorry)
      (ShortComplex.Splitting.r (σ (p + 1)) ≫
        𝟙 (S.X₁.X (p + 1)) ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
  𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
Tactic: dsimp at s_g 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
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))
⊢ 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)
have 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 sorry) 0
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]
-- 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 : ℤ
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))
⊢ 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
have 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 sorry) 0
Tactic: rw [← comp_f_assoc, S.zero, zero_f, zero_comp]
-- 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 : ℤ
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
⊢ 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
have 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 sorry) 0
Tactic: rw [← comp_f_assoc, S.zero, zero_f, zero_comp]
-- 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 : ℤ
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
⊢ 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
have rw₂ : Eq (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
  (0 ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p sorry) 0
Tactic: rw [← comp_f_assoc, S.zero, zero_f, zero_comp]
-- 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 : ℤ
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
⊢ 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
have rw₃ : Eq.{v + 1} (α := S.X₁.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p) 0 0
Tactic: rw [← comp_f_assoc, S.zero, zero_f, zero_comp]
-- 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 q : ℤ
hpq : 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) ≫
      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)
have 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 sorry)
      (ShortComplex.Splitting.r (σ (p + 1)) ≫
        (XIsoOfEq S.X₁ sorry).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) sorry ≫
        ShortComplex.Splitting.s (σ (p + 1)))
      (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p sorry ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) sorry) =
  𝟙 (S.X₂.X (p + 1))
Tactic: subst hpq
Cleared hypotheses: q, hpq
-- 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
p : ℤ
⊢ 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))
have 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))))
Tactic: have h := (σ (p + 1)).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
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))))
⊢ 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))
have 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 sorry)
      (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) sorry ≫
        ShortComplex.Splitting.s (σ (p + 1)))
      (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p sorry ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) sorry) =
  𝟙 (S.X₂.X (p + 1))
Tactic: dsimp at 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
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))
⊢ 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))
have 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)))
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]
-- 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
p : ℤ
⊢ 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))))
have 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))
Tactic: have r_f := (σ (p + 1 + 1)).r_f
-- 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
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))
⊢ 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))))
have 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))))
Tactic: have s_g := (σ (p + 1)).s_g
-- 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)) ≫ 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))))
⊢ 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))))
have dsimp : Eq (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
  (Iso.hom (mappingConeHomOfDegreewiseSplitXIso S σ p (p + 1) sorry) ≫
      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) sorry) :
    (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ S.X₂.X (p + 1 + 1))
Tactic: dsimp at r_f s_g ⊢
-- 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))
⊢ p + 1 + -1 = p
have linarith : p + 1 + -1 < p → -1 + (p + 1 + -1 + 1 - p) = 0
Tactic: linarith
-- 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))
linarith : p + 1 + -1 < p → -1 + (p + 1 + -1 + 1 - p) = 0
⊢ p + 1 + -1 = p
have linarith₁ : p < p + 1 + -1 → -1 + (p + 1 - (p + 1 + -1)) = 0
Tactic: linarith