awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ X.map θ
have h : Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶ X.obj Δ')
  (HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op) :
    HomologicalComplex.X K[X]
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      X.obj Δ')
  (HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map (A.e.op ≫ θ))
Tactic: simp only [← X.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶ X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op) :
      HomologicalComplex.X K[X]
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
        X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (A.e.op ≫ θ))
have h : Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op = A.e.op ≫ θ
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op = A.e.op ≫ θ
have h : ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ
Tactic: simp only [← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
    ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
      {
          app := fun (Δ : SimplexCategoryᵒᵖ) ↦
            Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
              HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                X.map A.e.op,
          naturality := ⋯ } ≫
        Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
    {
      app := fun (Δ : SimplexCategoryᵒᵖ) ↦
        Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op,
      naturality := ⋯ }
have h : ∀ (n : ℕ),
  Eq (α :=
    Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) _⦋n⦌)
    (Splitting.φ (Γ₀.splitting K[X])
      ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
        {
            app := fun (Δ : SimplexCategoryᵒᵖ) ↦
              Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
                HomologicalComplex.Hom.f PInfty
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                  X.map A.e.op,
            naturality := sorry } ≫
          Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      n)
    (Splitting.φ (Γ₀.splitting K[X])
      {
        app := fun (Δ : SimplexCategoryᵒᵖ) ↦
          Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
              X.map A.e.op,
        naturality := sorry }
      n)
Tactic: apply (Γ₀.splitting K[X]).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) _⦋n⦌)
    (Splitting.φ (Γ₀.splitting K[X])
      ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
        {
            app := fun (Δ : SimplexCategoryᵒᵖ) ↦
              Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
                HomologicalComplex.Hom.f PInfty
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                  X.map A.e.op,
            naturality := ⋯ } ≫
          Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      n)
    (Splitting.φ (Γ₀.splitting K[X])
      {
        app := fun (Δ : SimplexCategoryᵒᵖ) ↦
          Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
              X.map A.e.op,
        naturality := ⋯ }
      n)
have h : Eq (α := Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶ X _⦋n⦌)
  (Splitting.ι (Γ₀.splitting K[X]) n ≫
    CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
      (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          CategoryStruct.comp (Y := X.obj (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })))
            (HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len :
              HomologicalComplex.X K[X]
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                HomologicalComplex.X K[X]
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
            (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) (op ⦋n⦌)) A) :
        Γ₀.obj K[X] _⦋n⦌ ⟶ Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
      ((Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
              X.map A.e.op) ≫
          𝟙 (X _⦋n⦌) :
        Γ₀.Obj.obj₂ K[X] (op ⦋n⦌) ⟶ X _⦋n⦌))
  (Splitting.ι (Γ₀.splitting K[X]) n ≫
    Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
      HomologicalComplex.Hom.f PInfty
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op)
Tactic: dsimp [N₁]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
have rw : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
    Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
  (NatTrans.app Γ₂N₁.natTrans X)
  (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
    CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
        (Karoubi.decompId_i (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
      NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans)
          (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
        Karoubi.decompId_p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
Tactic: rw [Γ₂N₂.natTrans_app_f_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          (Karoubi.decompId_i (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
        NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans)
            (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
          Karoubi.decompId_p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
have dsimp : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
    Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
  (NatTrans.app Γ₂N₁.natTrans X)
  (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
    CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
        { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
          p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := sorry :
          Karoubi (SimplicialObject.{v_1, u_1} C) })
      (CategoryTheory.Functor.map Γ₂
        (CategoryTheory.Functor.map N₂ (𝟙 (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))))
      ((NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
            (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
          NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
        𝟙
          { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
            p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := sorry }))
Tactic: dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
    NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
            p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
            Karoubi (SimplicialObject.{v_1, u_1} C) })
        (CategoryTheory.Functor.map Γ₂
          (CategoryTheory.Functor.map N₂ (𝟙 (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))))
        ((NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ }))
have rw : NatTrans.app Γ₂N₁.natTrans X =
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    𝟙
        (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
          (Functor.obj N₂ (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
          NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
        𝟙
          { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
            p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := sorry :
            Karoubi (SimplicialObject.{v_1, u_1} C) }
Tactic: rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
              Karoubi (SimplicialObject.{v_1, u_1} C) }
have dsimp : NatTrans.app Γ₂N₁.natTrans X =
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    𝟙
        (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
          (Functor.obj N₂ { X := X, p := 𝟙 X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) })) ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫
        𝟙 { X := X, p := 𝟙 X, idem := sorry : Karoubi (SimplicialObject.{v_1, u_1} C) }
Tactic: dsimp only [toKaroubi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫
          𝟙 { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }
have erw : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶ { X := X, p := 𝟙 X, idem := sorry })
  (NatTrans.app Γ₂N₁.natTrans X)
  (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := sorry })
Tactic: erw [id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ })
have rw : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶ { X := X, p := 𝟙 X, idem := sorry })
  (NatTrans.app Γ₂N₁.natTrans X)
  (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X)
Tactic: rw [comp_id, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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 : SimplicialObject.{v_1, u_1} C
rw :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X)
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ })
have rw₁ : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶ { X := X, p := 𝟙 X, idem := sorry })
  (NatTrans.app Γ₂N₁.natTrans X) (NatTrans.app Γ₂N₁.natTrans X)
Tactic: rw [comp_id, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y := Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₂ P))) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₂ P))) n)
have eq₁ : Eq (α :=
  HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
    HomologicalComplex.X
      (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
  (HomologicalComplex.Hom.f PInfty n ≫
    P.p.app (op ⦋n⦌) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
        (Splitting.IndexSet.id (op ⦋n⦌)))
Tactic: have eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫
      ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
    simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]