awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
⊢ Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫
      𝟙 (sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A))
have rw : Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
  (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
  (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A })
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
have rw : θ.unop ≫ θ'.unop ≫ A.e = (θ.unop ≫ θ'.unop) ≫ A.e
Tactic: rw [unop_comp, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
rw : θ.unop ≫ θ'.unop ≫ A.e = (θ.unop ≫ θ'.unop) ≫ A.e
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
have rw₁ : θ.unop ≫ θ'.unop ≫ A.e = θ.unop ≫ θ'.unop ≫ A.e
Tactic: rw [unop_comp, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K (θ' ≫ θ))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K θ' ≫ Obj.map K θ)
have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
Tactic: have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e := by rw [unop_comp, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K (θ' ≫ θ))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K θ' ≫ Obj.map K θ)
have fac₁ : CategoryStruct.comp (Y := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
    (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
    (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) =
  (θ' ≫ θ).unop ≫ A.e
Tactic: rw [← image.fac (θ'.unop ≫ A.e), ← assoc, ←
      image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)), assoc] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  CategoryStruct.comp (Y := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) =
    (θ' ≫ θ).unop ≫ A.e
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K (θ' ≫ θ))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K θ' ≫ Obj.map K θ)
have simp : Eq (α :=
  Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
      { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
    Obj.obj₂ K Δ)
  (CategoryStruct.comp (Y := K.X (image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))).len)
    (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)))
    (Sigma.ι (Obj.summand K Δ)
      (Splitting.IndexSet.mk (Δ' := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
        (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))))))
  (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ (A.pull θ').e)).len)
    (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ (A.pull θ').e) ≫ image.ι (θ'.unop ≫ A.e)))
    (Sigma.ι (Obj.summand K Δ) ((A.pull θ').pull θ)))
Tactic: simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ,
      Obj.Termwise.mapMono_comp_assoc, Obj.map_on_summand₀ K A fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Eq (α :=
    Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A ⟶
      Cocone.pt (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
        (Splitting.cofan' (fun (n : ℕ) ↦ K.X n) (obj K)
          (fun (n : ℕ) ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ))
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
            (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))))))
    (Cofan.inj
      (Splitting.cofan' (fun (n : ℕ) ↦ K.X n) (obj K)
        (fun (n : ℕ) ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ)
      A)
have dsimp : Eq.{v_1 + 1} (α :=
  K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
  (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A ≫
      𝟙 (colimit.{0, 0, v_1, u_1} (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) :
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
  (Sigma.ι (Obj.summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
        (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
      Obj.map K A.e.op :
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
Tactic: dsimp [Splitting.cofan']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A ≫
        𝟙 (colimit.{0, 0, v_1, u_1} (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Sigma.ι (Obj.summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
          (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
        Obj.map K A.e.op :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
have rw : Eq.{v_1 + 1} (α :=
  K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
  (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
    Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
      (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
        (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
  (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
    Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
Tactic: rw [comp_id, Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl), Γ₀.Obj.Termwise.mapMono_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
      Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
        (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
          (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
    (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
have rw : Eq.{v_1 + 1} (α :=
  K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
  (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A)
  (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ A ⟶ (obj K).obj Δ')
    (Cofan.inj (Splitting.cofan (splitting K) Δ) A ≫ (obj K).map θ)
    (Termwise.mapMono K i ≫ Cofan.inj (Splitting.cofan (splitting K) Δ') (Splitting.IndexSet.mk e))
have dsimp : Eq (α :=
  Splitting.N (X := obj K) (splitting K)
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    obj₂ K Δ')
  ((Splitting.ι (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      map K A.e.op) ≫
    map K θ)
  (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
Tactic: dsimp [Splitting.cofan]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      obj₂ K Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        map K A.e.op) ≫
      map K θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
have change : Eq (α :=
  Splitting.N (X := obj K) (splitting K)
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    (obj K).obj Δ')
  ((Splitting.ι (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (obj K).map A.e.op) ≫
    (obj K).map θ)
  (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
Tactic: change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        (obj K).map A.e.op) ≫
      (obj K).map θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
have rw : Eq (α :=
  Splitting.N (X := obj K) (splitting K)
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    (obj K).obj Δ')
  (Splitting.ι (splitting K)
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    (obj K).map (A.e.op ≫ θ))
  (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
Tactic: rw [assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    (Splitting.ι (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (obj K).map (A.e.op ≫ θ))
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
have dsimp : Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Sigma.ι (summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
        (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
      map K (A.e.op ≫ θ) :
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op :
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
Tactic: dsimp [splitting]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i =
    (A.e.op ≫ θ).unop ≫
      𝟙 (unop (op (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))))
have rw : θ.unop ≫ A.e = (A.e.op ≫ θ).unop
Tactic: rw [comp_id, fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Sigma.ι (summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
          (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
        map K (A.e.op ≫ θ) :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
        Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
have rw : Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
  (Termwise.mapMono K i ≫
    Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op)
Tactic: rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
    (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op)
have dsimp : Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Termwise.mapMono K i ≫
    Sigma.ι (summand K Δ')
      (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
        (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e sorry)))
  (Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op)
Tactic: dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op)
have rw : Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Termwise.mapMono K i ≫
    Sigma.ι (summand K Δ')
      (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
        (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e sorry)))
  (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
Tactic: rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ''))
      (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp), Termwise.mapMono_id]