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
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h :
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) 0
pos :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋n⦌)))
        (CategoryStruct.comp (Y := X _⦋n⦌)
          (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
            summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n)))
    0
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (CategoryStruct.comp (Y :=
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋n⦌)))).len)
            (s.πSummand (IndexSet.id (op ⦋n⦌))) (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
have pos₁ : Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
  (CategoryStruct.comp (Y :=
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }) (IndexSet.id (op ⦋n⦌)))).len)
    0
    (CategoryStruct.comp (Y := X _⦋n⦌)
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n)))
  0
Tactic: rw [assoc, reassoc_of% h, zero_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
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h :
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) 0
pos :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋n⦌)))
        (CategoryStruct.comp (Y := X _⦋n⦌)
          (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
            summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n)))
    0
pos₁ :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      0
      (CategoryStruct.comp (Y := X _⦋n⦌)
        (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
          summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n)))
    0
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (CategoryStruct.comp (Y :=
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋n⦌)))).len)
            (s.πSummand (IndexSet.id (op ⦋n⦌))) (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
have pos₂ : Eq.{v_1 + 1} (α := Z ⟶ HomologicalComplex.X K[X] n) 0 0
Tactic: rw [assoc, reassoc_of% h, zero_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 : ℕ
| s.πSummand (IndexSet.id (op ⦋n⦌))
have rw : 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))
Tactic: rw [← id_comp (s.πSummand _)]
-- 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 (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) (s.πSummand (IndexSet.id (op ⦋n⦌)))
have conv_rhs : Eq (α :=
  HomologicalComplex.X K[X] n ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋n⦌)))).len)
  (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
  (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
Tactic: conv_rhs => rw [← id_comp (s.πSummand _)]
-- 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 (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have symm : Eq (α :=
  HomologicalComplex.X K[X] n ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋n⦌)))).len)
  (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
  (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
Tactic: symm
-- 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 (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw : HSub.hSub (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (β :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₁ : Eq (α :=
  HomologicalComplex.X K[X] n ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋n⦌)))).len)
  (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
    s.πSummand (IndexSet.id (op ⦋n⦌)))
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₂ : Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
  (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
    HomologicalComplex.Hom.f PInfty n)
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
rw₂ :
  Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₃ : HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
    (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
rw₂ :
  Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₃ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₄ : HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
    (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
rw₂ :
  Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₃ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
rw₄ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₅ : HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
    (HomologicalComplex.Hom.f PInfty n) =
  0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
rw₂ :
  Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₃ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
rw₄ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
rw₅ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n) =
    0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
have rw₆ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) 0 0
Tactic: rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]
-- 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 : ℕ
| HomologicalComplex.Hom.f PInfty n
have rw : 𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
Tactic: rw [← id_comp (PInfty.f n)]
-- 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⦌ ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋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)))
    (HomologicalComplex.Hom.f PInfty n)
have conv_rhs : CategoryStruct.comp (Y :=
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋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)) =
  𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
Tactic: conv_rhs => rw [← id_comp (PInfty.f n)]
-- 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 : ℕ
⊢ CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋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)) =
    𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
have dsimp : 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⦌)
Tactic: dsimp only [AlternatingFaceMapComplex.obj_X]