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
n : ℕ
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋n⦌)))
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) (HomologicalComplex.Hom.f PInfty n)) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)
have rw : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y :=
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }) (IndexSet.id (op ⦋n⦌)))).len)
    (s.πSummand (IndexSet.id (op ⦋n⦌)))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) (HomologicalComplex.Hom.f PInfty n)))
  (∑ j : IndexSet (op ⦋n⦌),
    CategoryStruct.comp (Y := X _⦋n⦌)
      (s.πSummand j ≫ Cofan.inj (s.cofan (op ⦋n⦌)) j :
        X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
Tactic: rw [s.decomposition_id, Preadditive.sum_comp]
-- 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
n : ℕ
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋n⦌)))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) (HomologicalComplex.Hom.f PInfty n)))
    (∑ j : IndexSet (op ⦋n⦌),
      CategoryStruct.comp (Y := X _⦋n⦌)
        (s.πSummand j ≫ Cofan.inj (s.cofan (op ⦋n⦌)) j :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
have rw : ∀ (x : IndexSet (op ⦋n⦌)),
  x ≠ IndexSet.id (op ⦋n⦌) →
    Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
        (s.πSummand x ≫ Cofan.inj (s.cofan (op ⦋n⦌)) x :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
      0
Tactic: rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]
-- 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
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
      (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋n⦌)) A :
        X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    0
have rw : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
  (s.πSummand A ≫
    CategoryStruct.comp (Y := X _⦋n⦌)
      (Cofan.inj (s.cofan (op ⦋n⦌)) A :
        summand s.N (op ⦋n⦌) A ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
  0
Tactic: rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, 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
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
rw :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (s.πSummand A ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (Cofan.inj (s.cofan (op ⦋n⦌)) A :
          summand s.N (op ⦋n⦌) A ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
      (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋n⦌)) A :
        X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    0
have rw₁ : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (s.πSummand A ≫ 0) 0
Tactic: rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, 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
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
rw :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (s.πSummand A ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (Cofan.inj (s.cofan (op ⦋n⦌)) A :
          summand s.N (op ⦋n⦌) A ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
rw₁ : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (s.πSummand A ≫ 0) 0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
      (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋n⦌)) A :
        X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    0
have rw₂ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) 0 0
Tactic: rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]
-- 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
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬A.EqId
⊢ 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 hA₁ : ¬Mono A.e
Tactic: rw [A.eqId_iff_mono] 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
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ 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 (α :=
  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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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
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
⊢ 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 (α := 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
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]