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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α :=
    S₁.s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ⟶
      S₂.s.N j)
    (Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)) :
          Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have pos : Φ.f
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
            (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
    𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
  CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
Tactic: rw [Splitting.cofan_inj_πSummand_eq_id]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
have pos : Φ.f j ≫ 𝟙 (S₂.s.N j) =
  CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j ≫ 𝟙 (S₂.s.N j) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
have pos : Φ.f j =
  CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
Tactic: rw [comp_id, Splitting.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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
pos :
  Φ.f j =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
⊢ Φ.f j ≫ 𝟙 (S₂.s.N j) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
have pos₁ : Φ.f j = Φ.f j
Tactic: rw [comp_id, Splitting.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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have neg : Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
    CategoryStruct.comp (Y := S₂.X _⦋j⦌)
      (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
        Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
      (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) =
  0 ≫ Φ.f j
Tactic: rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), 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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
neg :
  Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) =
    0 ≫ Φ.f j
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have neg₁ : Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
  (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0)
  (0 ≫ Φ.f j)
Tactic: rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), 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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
neg :
  Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) =
    0 ≫ Φ.f j
neg₁ :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0)
    (0 ≫ Φ.f j)
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have neg₂ : Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
  (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
Tactic: rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), 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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
neg :
  Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) =
    0 ≫ Φ.f j
neg₁ :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0)
    (0 ≫ Φ.f j)
neg₂ :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have neg₃ : Eq.{v_1 + 1} (α :=
  S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j) 0 0
Tactic: rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), 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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)
      (Functor.obj (forget C ⋙ N₁) Y))
    (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
      Iso.hom
        ((fun (S : Split.{v_1, u_1} C) ↦
            (S.s.toKaroubiNondegComplexIsoN₁ :
              Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
          Y))
    (Iso.hom
        ((fun (S : Split.{v_1, u_1} C) ↦
            (S.s.toKaroubiNondegComplexIsoN₁ :
              Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
          X) ≫
      Functor.map (forget C ⋙ N₁) Φ)
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X))
        n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (forget C ⋙ N₁) Y)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
          Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              Y)))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              X) ≫
          Functor.map (forget C ⋙ N₁) Φ))
      n)
Tactic: ext n
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X))
        n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (forget C ⋙ N₁) Y)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
          Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              Y)))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              X) ≫
          Functor.map (forget C ⋙ N₁) Φ))
      n)
have h : Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
  (Φ.f n ≫
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
      (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
  (CategoryStruct.comp (Y := X.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n) :
      X.s.N n ⟶ X.X _⦋n⦌)
    (CategoryStruct.comp (Y := X.X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n)
        (Φ.F.app (op ⦋n⦌)) :
      X.X _⦋n⦌ ⟶ Y.X _⦋n⦌))
Tactic: dsimp
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := X.X _⦋n⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
            Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n) :
        X.s.N n ⟶ X.X _⦋n⦌)
      (CategoryStruct.comp (Y := X.X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n)
          (Φ.F.app (op ⦋n⦌)) :
        X.X _⦋n⦌ ⟶ Y.X _⦋n⦌))
have h : Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
  (Φ.f n ≫
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
      (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
Tactic: simp only [assoc, PInfty_f_idem_assoc]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
have h : Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (Φ.F.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) :
    Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
Tactic: erw [← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
        (Φ.F.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
have h : Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌)) :
    Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
Tactic: rw [PInfty_f_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
⊢ ed.section_.app n ≫ X.hom.app n = 𝟙 X.right
have dsimp : (ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from (unop n)))) ≫ X.hom.app n = 𝟙 X.right
Tactic: dsimp [section_]