awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(unop
          ((A.epiComp (SimplexCategory.σ i).op).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
            { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α }))).len =
      (unop (op ⦋n + 1⦌)).len
have h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≤ (unop (op ⦋n⦌)).len
Tactic: have h := SimplexCategory.len_le_of_epi A.e
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h :
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≤
    (unop (op ⦋n⦌)).len
⊢ ¬(unop
          ((A.epiComp (SimplexCategory.σ i).op).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
            { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α }))).len =
      (unop (op ⦋n + 1⦌)).len
have h₁ : ¬(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len = n + 1
Tactic: dsimp at h ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0
have hA₁ : ¬Mono A.e
Tactic: rw [SimplicialObject.Splitting.IndexSet.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
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0
have rw : Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
  ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op) ≫
    HomologicalComplex.Hom.f PInfty n)
  0
Tactic: rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e 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
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
rw :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0
have rw₁ : Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
  (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
    X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty n)
  0
Tactic: rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e 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
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
rw :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₁ :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty n)
    0
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0
have rw₂ : Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
  (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
Tactic: rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e 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
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
rw :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₁ :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty n)
    0
rw₂ :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0
have rw₃ : Eq.{v_1 + 1} (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n) 0 0
Tactic: rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e 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
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 ↔
    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
have mp : Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 →
  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
Tactic: constructor
-- 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⦌
mp :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 →
    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
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 ↔
    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
have mpr : 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 →
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
Tactic: constructor
-- 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 ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
⊢ 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
have mp : ∀ (f : Z ⟶ X _⦋0⦌) (h : Eq (α := Z ⟶ HomologicalComplex.X K[X] 0) (f ≫ HomologicalComplex.Hom.f PInfty 0) 0),
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
Tactic: rcases n with _ | n
Cleared hypotheses: n, f, h
-- 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 ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
mp :
  ∀ (f : Z ⟶ X _⦋0⦌) (h : Eq (α := Z ⟶ HomologicalComplex.X K[X] 0) (f ≫ HomologicalComplex.Hom.f PInfty 0) 0),
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋0⦌)))).len)
      (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
⊢ 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
have mp₁ : ∀ (n : ℕ) (f : Z ⟶ X _⦋n + 1⦌)
  (h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0),
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
Tactic: rcases n with _ | n
Cleared hypotheses: n, f, h
-- 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
Z : C
f : Z ⟶ X _⦋0⦌
h : f ≫ 𝟙 (X _⦋0⦌) = 0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
have h₁ : f = 0
Tactic: rw [comp_id] at h
Cleared hypotheses: h
-- 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
f : Z ⟶ X _⦋0⦌
h : f = 0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
have mp : Eq (α :=
  Z ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋0⦌)))).len)
  (0 ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
Tactic: rw [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
f : Z ⟶ X _⦋0⦌
h : f = 0
mp :
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (0 ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
have mp₁ : Eq.{v_1 + 1} (α :=
  Z ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋0⦌)))).len)
  0 0
Tactic: rw [h, zero_comp]
-- 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
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
have h' : f ≫
    HAdd.hAdd (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) =
  f ≫ 𝟙 (HomologicalComplex.X K[X] (n + 1))
Tactic: have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
-- 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
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' :
  f ≫
      HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (HomologicalComplex.Hom.f PInfty (n + 1))
        (HomologicalComplex.Hom.f QInfty (n + 1)) =
    f ≫ 𝟙 (X _⦋n + 1⦌)
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
have h'₁ : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
Tactic: rw [comp_id, comp_add, h, zero_add] at h'
Cleared hypotheses: h'
-- 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 + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
have mp : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < n + 1} x →
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n + 1⦌)))).len)
      (f ≫
        (HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫
          s.πSummand (IndexSet.id (op ⦋n + 1⦌)))
      0
Tactic: rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
        Finset.sum_eq_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
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
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
have mpr : ∀ (a : IndexSet (op ⦋n⦌)),
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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
Tactic: rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_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
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
A : IndexSet (op ⦋n⦌)
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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 pos : ∀ (hA : A.EqId),
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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
Tactic: by_cases hA : A.EqId
-- 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
A : IndexSet (op ⦋n⦌)
pos :
  ∀ (hA : A.EqId),
    Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
      (f ≫
        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
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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 neg : ∀ (hA : ¬A.EqId),
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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
Tactic: by_cases hA : A.EqId
-- 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
A : IndexSet (op ⦋n⦌)
hA : A = IndexSet.id (op ⦋n⦌)
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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 pos : 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
Tactic: subst hA
Cleared hypotheses: A, 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
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
⊢ 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)
  (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
Tactic: rw [assoc, reassoc_of% h, zero_comp]