awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
q : ℕ
hq :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P (q + 1))
    (P (q + 1) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have succ : HAdd.hAdd (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ Hσ q) =
  HAdd.hAdd (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
    (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
Tactic: simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
q : ℕ
hq :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ Hσ q) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have succ : HAdd.hAdd (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
    (P q ≫ NatTrans.app (natTransHσ q) x ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) =
  HAdd.hAdd (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
    (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
Tactic: erw [(natTransHσ q).naturality f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
q : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have zero : Eq (α :=
  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
    (Functor.obj (alternatingFaceMapComplex C) x_1))
  (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P 0)
  (P 0 ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
Tactic: induction q with
    | zero =>
      dsimp [alternatingFaceMapComplex]
      simp only [P_zero, id_comp, comp_id]
    | succ q hq =>
      simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
      -- `erw` is needed to see through `natTransHσ q).app = Hσ q`
      erw [(natTransHσ q).naturality f]
      rfl
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
q : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
zero :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P 0)
    (P 0 ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have succ : ∀ (q : ℕ)
  (hq :
    Eq (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)),
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P (q + 1))
    (P (q + 1) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
Tactic: induction q with
    | zero =>
      dsimp [alternatingFaceMapComplex]
      simp only [P_zero, id_comp, comp_id]
    | succ q hq =>
      simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
      -- `erw` is needed to see through `natTransHσ q).app = Hσ q`
      erw [(natTransHσ q).naturality f]
      rfl
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] n) (f.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f (Q q) n)
    (HomologicalComplex.Hom.f (Q q) n ≫ f.app (op ⦋n⦌))
have simp : f.app (op ⦋n⦌) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app (op ⦋n⦌)
Tactic: simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality,
    sub_comp, sub_left_inj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app (op ⦋n⦌)
have dsimp : f.app (op ⦋n⦌) ≫ 𝟙 (Y _⦋n⦌) = 𝟙 (X _⦋n⦌) ≫ f.app (op ⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P 0) n)) (HomologicalComplex.Hom.f (P 0) n)
have zero : Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
  (G.map (HomologicalComplex.Hom.f (𝟙 K[X]) n))
  (HomologicalComplex.Hom.f (𝟙 K[(Functor.obj (whiskering C D) G).obj X]) n)
Tactic: simp only [P_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)
have zero : Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
  (G.map (HomologicalComplex.Hom.f (P 0) n)) (HomologicalComplex.Hom.f (P 0) n)
Tactic: induction q with
  | zero =>
    simp only [P_zero]
    apply G.map_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
zero :
  Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P 0) n)) (HomologicalComplex.Hom.f (P 0) n)
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)
have succ : ∀ (q : ℕ)
  (hq :
    Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
      (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)),
  Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P (q + 1)) n)) (HomologicalComplex.Hom.f (P (q + 1)) n)
Tactic: induction q with
  | zero =>
    simp only [P_zero]
    apply G.map_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (Q q) n)) (HomologicalComplex.Hom.f (Q q) n)
have rw : G.map (𝟙 (X _⦋n⦌)) = 𝟙 ((Functor.obj (whiskering C D) G).obj X _⦋n⦌)
Tactic: rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f,
    P_add_Q_f]
-- 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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have pos : (h : B = A) →
  s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: by_cases h : B = A
-- 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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
pos :
  (h : B = A) →
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have neg : (h : ¬B = A) →
  s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: by_cases h : B = A
-- 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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len =
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have subst : s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len =
  s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: subst h
Cleared hypotheses: A, 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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B = 0
have dsimp : Eq (α :=
  s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
  ((s.cofan Δ).inj A ≫ s.desc Δ fun (B_1 : IndexSet Δ) ↦ if h : B_1 = B then eqToHom sorry else 0) 0
Tactic: dsimp [π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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ Eq (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    ((s.cofan Δ).inj A ≫ s.desc Δ fun (B_1 : IndexSet Δ) ↦ if h : B_1 = B then eqToHom ⋯ else 0) 0
have rw : Eq.{v_1 + 1} (α :=
  s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
  (if h : A = B then eqToHom sorry else 0) 0
Tactic: rw [ι_desc, dif_neg h.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 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
rw :
  Eq.{v_1 + 1} (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    (if h : A = B then eqToHom ⋯ else 0) 0
⊢ Eq (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    ((s.cofan Δ).inj A ≫ s.desc Δ fun (B_1 : IndexSet Δ) ↦ if h : B_1 = B then eqToHom ⋯ else 0) 0
have rw₁ : Eq.{v_1 + 1} (α :=
  s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
  0 0
Tactic: rw [ι_desc, dif_neg h.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
Δ : SimplexCategoryᵒᵖ
⊢ Eq.{v_1 + 1} (α := X.obj Δ ⟶ X.obj Δ) (𝟙 (X.obj Δ)) (∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A)
have h : ∀ (A : IndexSet Δ),
  (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
Tactic: apply s.hom_ext'
-- 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
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
have h : ∀ (b : IndexSet Δ),
  Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ b →
    b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0
Tactic: erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_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
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h :
  ∀ (b : IndexSet Δ),
    Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ b →
      b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
have h₁ : A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0
Tactic: erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_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
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ B
h₂ : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0
have h : Eq (α := s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ X.obj Δ)
  (0 ≫ (s.cofan Δ).inj B) 0
Tactic: rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ 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
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h_1 : Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ B
h₂ : B ≠ A
h :
  Eq (α := s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ X.obj Δ)
    (0 ≫ (s.cofan Δ).inj B) 0
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0
have h₁ : Eq.{v_1 + 1} (α :=
  s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ X.obj Δ) 0 0
Tactic: rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ 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 : ℕ
i : Fin (n + 1)
⊢ Eq (α :=
    X _⦋n⦌ ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
have h : ∀ (A : IndexSet (op ⦋n⦌)),
  Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
Tactic: apply s.hom_ext'
-- 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⦌)
⊢ Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
have h : Eq (α :=
  summand s.N (op ⦋n⦌) A ⟶
    s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n + 1⦌ ⟶ unop Δ' // Epi α })
            (IndexSet.id (op ⦋n + 1⦌)))).len)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
    (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
    (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
Tactic: dsimp only [SimplicialObject.σ]
-- 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⦌)
⊢ Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n + 1⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
have h : IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op
Tactic: rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,
    cofan_inj_πSummand_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
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op
have h : A.epiComp (SimplexCategory.σ i).op ≠ IndexSet.id (op ⦋n + 1⦌)
Tactic: rw [ne_comm]
-- 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⦌)
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId
have h : ¬(unop
        ((A.epiComp (SimplexCategory.σ i).op).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
          { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α }))).len =
    (unop (op ⦋n + 1⦌)).len
Tactic: rw [IndexSet.eqId_iff_len_eq]