awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
rw :
  Eq (α :=
    summand s.N (op ⦋j⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k) ≫
      s.πSummand (IndexSet.id (op ⦋k⦌)))
    0
rw₁ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k) ≫
      HomologicalComplex.Hom.f PInfty k)
    0
rw₂ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k ≫ HomologicalComplex.Hom.f PInfty k))
    0
rw₃ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k))
    0
rw₄ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k)
    0
rw₅ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty j ≫ HomologicalComplex.d K[X] j k)
    0
rw₆ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      0 ≫ HomologicalComplex.d K[X] j k)
    0
rw₇ :
  Eq (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
⊢ Eq (α :=
    summand s.N (op ⦋j⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (Cofan.inj (s.cofan (op ⦋j⦌)) A) (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))))
    0
have rw₈ : Eq.{v_1 + 1} (α := summand s.N (op ⦋j⦌) A ⟶ HomologicalComplex.X K[X] k) 0 0
Tactic: rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.cofan_inj_eq, assoc,
    degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
⊢ s.d i j ≫ s.d j k = 0
have simp : Eq (α := s.N i ⟶ s.N k)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
      (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
        summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
          (CategoryStruct.comp (Y := s.N j)
            (s.πSummand (IndexSet.id (op ⦋j⦌)) :
              X _⦋j⦌ ⟶
                s.N
                  (unop
                      (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                        (IndexSet.id (op ⦋j⦌)))).len)
            (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
              (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                  (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
        Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
    s.N i ⟶ s.N k)
  (0 : s.N i ⟶ s.N k)
Tactic: simp only [d, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
⊢ Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
have eq : Eq (α :=
  HomologicalComplex.X K[X] i ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋k⦌)))).len)
  (HomologicalComplex.d K[X] i j ≫ 𝟙 (X _⦋j⦌) ≫ HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))) 0
Tactic: have eq : K[X].d i j ≫ 𝟙 (X.obj (op ⦋j⦌)) ≫ K[X].d j k ≫
        s.πSummand (IndexSet.id (op ⦋k⦌)) = 0 := by
      simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫ 𝟙 (X _⦋j⦌) ≫ HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))) 0
⊢ Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
have eq₁ : Eq (α :=
  HomologicalComplex.X K[X] i ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋k⦌)))).len)
  (HomologicalComplex.d K[X] i j ≫
    CategoryStruct.comp (Y := X _⦋j⦌)
      (∑ A : IndexSet (op ⦋j⦌), s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋j⦌)) A :
        X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
      (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
        X _⦋j⦌ ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋k⦌)))).len))
  0
Tactic: rw [s.decomposition_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  HAdd.hAdd (α :=
      HomologicalComplex.X K[X] i ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋k⦌)))).len)
      (HomologicalComplex.d K[X] i j ≫
        CategoryStruct.comp (Y :=
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋j⦌)))).len)
          (s.πSummand (IndexSet.id (op ⦋j⦌)))
          (CategoryStruct.comp (Y := X _⦋j⦌)
            (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
              summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))))
      (∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        HomologicalComplex.d K[X] i j ≫
          CategoryStruct.comp (Y := X _⦋j⦌)
            (s.πSummand j_1 ≫ Cofan.inj (s.cofan (op ⦋j⦌)) j_1 :
              X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))) =
    0
A : IndexSet (op ⦋j⦌)
hA : Membership.mem (γ := Finset (IndexSet (op ⦋j⦌))) {IndexSet.id (op ⦋j⦌)}ᶜ A
⊢ Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫
      CategoryStruct.comp (Y := X _⦋j⦌)
        (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋j⦌)) A :
          X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))))
    0
have hA₁ : ¬A = IndexSet.id (op ⦋j⦌)
Tactic: simp only [Finset.mem_compl, Finset.mem_singleton] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫
      CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋j⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋j⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌)
          (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
            summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
          (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))))
    0
⊢ Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
have rw : Eq (α := s.N i ⟶ s.N k)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
      (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌))) 0 :
    s.N i ⟶ s.N k)
  (0 : s.N i ⟶ s.N k)
Tactic: rw [eq, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫
      CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋j⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋j⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌)
          (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
            summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
          (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))))
    0
rw :
  Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌))) 0 :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
⊢ Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
have rw₁ : Eq.{v_1 + 1} (α := s.N i ⟶ s.N k) 0 0
Tactic: rw [eq, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)
    ((Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) ≫ HomologicalComplex.Hom.f PInfty i) ≫
        HomologicalComplex.d (Karoubi.X (Functor.obj N₁ X)) i j :
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)
    (HomologicalComplex.d (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i j ≫
        Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) ≫ HomologicalComplex.Hom.f PInfty j :
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)
have dsimp : Eq (α := s.N i ⟶ X _⦋j⦌)
  (CategoryStruct.comp (Y := X _⦋i⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i))
      (HomologicalComplex.d K[X] i j) :
    s.N i ⟶ X _⦋j⦌)
  (CategoryStruct.comp (Y := s.N j)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
            summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j) :
        s.N i ⟶ s.N j)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
          (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
            summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
          (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j) :
        s.N j ⟶ X _⦋j⦌) :
    s.N i ⟶ X _⦋j⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
      (Karoubi.X (Functor.obj N₁ X)))
    (Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) ≫
      { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
          comm' := ⋯ } ≫
        Karoubi.p (Functor.obj N₁ X))
    { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
      comm' := ⋯ }
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) ≫
        { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
            comm' := sorry } ≫
          Karoubi.p (Functor.obj N₁ X))
      n)
    (HomologicalComplex.Hom.f
      { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
        comm' := sorry }
      n)
Tactic: ext n