awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
n : ℕ
rw :
  Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
      HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex A) X) (n + 1) n)
    (HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n)
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X N[X] n)
    (CategoryStruct.comp (Y := HomologicalComplex.X N[X] (n + 1))
      ((fun (n : ℕ) ↦ (NormalizedMooreComplex.objX X n).factorThru (HomologicalComplex.Hom.f PInfty n) ⋯) (n + 1))
      (HomologicalComplex.d N[X] (n + 1) n))
    (HomologicalComplex.d K[X] (n + 1) n ≫
      (fun (n : ℕ) ↦ (NormalizedMooreComplex.objX X n).factorThru (HomologicalComplex.Hom.f PInfty n) ⋯) n)

Tactic:
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow,
      ← inclusionOfMooreComplexMap_f, NormalizedMooreComplex.obj_d, ChainComplex.of_d,
      ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
      inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, alternatingFaceMapComplex_obj_d,
      ← alternatingFaceMapComplex_obj_d]

Premises used: AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.Category.assoc, CategoryTheory.Subobject.arrow, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.Subobject.factorThru_arrow_assoc, CategoryTheory.cancel_mono, AlgebraicTopology.normalizedMooreComplex_objD, HAdd.hAdd, AlgebraicTopology.inclusionOfMooreComplexMap, CategoryTheory.Subobject.factorThru_arrow, AlgebraicTopology.NormalizedMooreComplex.objX, OfNat.ofNat, ChainComplex.of_d, AlgebraicTopology.inclusionOfMooreComplexMap_f, HomologicalComplex.Hom.comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
      HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex A) X) (n + 1) n)
    (HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n)

Tactic:
PInfty.comm (n + 1) n

Premises used: AlgebraicTopology.DoldKan.PInfty, HAdd.hAdd, OfNat.ofNat, HomologicalComplex.Hom.comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
      HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex A) X) (n + 1) n)
    (HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n)

Tactic:
exact PInfty.comm (n + 1) n

Premises used: AlgebraicTopology.DoldKan.PInfty, HAdd.hAdd, OfNat.ofNat, HomologicalComplex.Hom.comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
h :
  Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0)
h₁ :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (n + 1))
      (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (n + 1))
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X) K[X])
    (inclusionOfMooreComplexMap X ≫ PInfty) (inclusionOfMooreComplexMap X)

Tactic:
ext (_ | n)
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
h :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
      X.obj (Opposite.op { len := 0 : SimplexCategory }))
    (CategoryStruct.comp (Y := X.obj (Opposite.op { len := 0 }))
        (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
          HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex A) X) 0)
        (𝟙 (X.obj (Opposite.op { len := 0 : SimplexCategory }))) :
      Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
        X.obj (Opposite.op { len := 0 : SimplexCategory }))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
      HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X K[X] 0)
⊢ Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
      X.obj (Opposite.op { len := 0 : SimplexCategory }))
    (CategoryStruct.comp (Y := X.obj (Opposite.op { len := 0 }))
        (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
          HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex A) X) 0)
        (𝟙 (X.obj (Opposite.op { len := 0 : SimplexCategory }))) :
      Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
        X.obj (Opposite.op { len := 0 : SimplexCategory }))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
      HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X K[X] 0)

Tactic:
simp only [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (n + 1))

Tactic:
(HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (n + 1))

Tactic:
exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
h : ∀ (n : ℕ), x.f n = x_1.f n
⊢ x = x_1

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
h : x.f n = x_1.f n
⊢ x.f n = x_1.f n

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
h : x.f n ≫ (NormalizedMooreComplex.objX X n).arrow = x_1.f n ≫ (NormalizedMooreComplex.objX X n).arrow
⊢ x.f n = x_1.f n

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x.f n ≫ (NormalizedMooreComplex.objX X n).arrow = x_1.f n ≫ (NormalizedMooreComplex.objX X n).arrow

Tactic:
HomologicalComplex.congr_hom hf n

Premises used: CategoryTheory.Subobject.arrow, HomologicalComplex.congr_hom
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x.f n ≫ (NormalizedMooreComplex.objX X n).arrow = x_1.f n ≫ (NormalizedMooreComplex.objX X n).arrow

Tactic:
exact HomologicalComplex.congr_hom hf n

Premises used: HomologicalComplex.congr_hom
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X)
      (Functor.obj (normalizedMooreComplex A) X))
    (inclusionOfMooreComplexMap X ≫ PInftyToNormalizedMooreComplex X) (𝟙 (Functor.obj (normalizedMooreComplex A) X))

Tactic:
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, CategoryTheory.cancel_mono, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.inclusionOfMooreComplexMap, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
w :
  ∀ (X : SimplicialObject.{v_1, u_1} A),
    Eq (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Karoubi.X (Functor.obj N₁ X)) (Karoubi.X (Functor.obj N₁ X)))
      (Karoubi.Hom.f
        (NatTrans.app
          ({
              app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                { f := PInftyToNormalizedMooreComplex X, comm := ⋯ :
                  Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj N₁ X)
                    (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) },
              naturality := ⋯ :
              NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁
                (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) } ≫
            { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ },
              naturality := ⋯ })
          X))
      (Karoubi.Hom.f (NatTrans.app (𝟙 N₁) X))
⊢ Eq (α := Quiver.Hom (V := SimplicialObject.{v_1, u_1} A ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ N₁)
    ({
        app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
          { f := PInftyToNormalizedMooreComplex X, comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj N₁ X)
              (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) },
        naturality := ⋯ :
        NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁
          (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) } ≫
      { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 N₁)

Tactic:
ext X : 3
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Karoubi.X (Functor.obj N₁ X)) (Karoubi.X (Functor.obj N₁ X)))
    (Karoubi.Hom.f
      (NatTrans.app
        ({
            app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
              { f := PInftyToNormalizedMooreComplex X, comm := ⋯ :
                Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj N₁ X)
                  (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) },
            naturality := ⋯ :
            NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁
              (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) } ≫
          { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ },
            naturality := ⋯ })
        X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 N₁) X))

Tactic:
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p, NatTrans.id_app, Karoubi.id_f]

Premises used: AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
w :
  ∀ (X : SimplicialObject.{v_1, u_1} A),
    Eq (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
        (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
        (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
      (Karoubi.Hom.f
        (NatTrans.app
          ({
              app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                  Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                    (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                    (Functor.obj N₁ X) },
              naturality := ⋯ :
              NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
                (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
            { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
              naturality := ⋯ })
          X))
      (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X))
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} A ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)))
    ({
        app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
          { f := inclusionOfMooreComplexMap X, comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
              (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
              (Functor.obj N₁ X) },
        naturality := ⋯ :
        NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
          (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
      { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)))

Tactic:
ext X : 3
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
w :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Functor.obj (alternatingFaceMapComplex A) X))
    (CategoryStruct.comp (Y := Functor.obj (normalizedMooreComplex A) X)
      (Karoubi.Hom.f
          (NatTrans.app
            ({
                app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                  { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                    Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                      (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                      (Functor.obj N₁ X) },
                naturality := ⋯ :
                NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
                  (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
              { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
                naturality := ⋯ })
            X) :
        Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
      (inclusionOfMooreComplexMap X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X) ≫
      inclusionOfMooreComplexMap X)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
    (Karoubi.Hom.f
      (NatTrans.app
        ({
            app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
              { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                  (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                  (Functor.obj N₁ X) },
            naturality := ⋯ :
            NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
              (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
          { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
            naturality := ⋯ })
        X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X))

Tactic:
rw [← cancel_mono (inclusionOfMooreComplexMap X)]

Premises used: CategoryTheory.cancel_mono, AlgebraicTopology.inclusionOfMooreComplexMap
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
w :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Functor.obj (alternatingFaceMapComplex A) X))
    (inclusionOfMooreComplexMap X)
    (Karoubi.p (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) ≫
      inclusionOfMooreComplexMap X)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Functor.obj (alternatingFaceMapComplex A) X))
    (CategoryStruct.comp (Y := Functor.obj (normalizedMooreComplex A) X)
      (Karoubi.Hom.f
          (NatTrans.app
            ({
                app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                  { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                    Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                      (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                      (Functor.obj N₁ X) },
                naturality := ⋯ :
                NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
                  (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
              { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
                naturality := ⋯ })
            X) :
        Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
      (inclusionOfMooreComplexMap X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X) ≫
      inclusionOfMooreComplexMap X)

Tactic:
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.Normalized
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
w w₁ :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X)
      (Functor.obj (alternatingFaceMapComplex A) X))
    (inclusionOfMooreComplexMap X) (inclusionOfMooreComplexMap X)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X)
      (Functor.obj (alternatingFaceMapComplex A) X))
    (inclusionOfMooreComplexMap X) (𝟙 (Functor.obj (normalizedMooreComplex A) X) ≫ inclusionOfMooreComplexMap X)

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
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 : ℕ
hqn : 0 ≤ q
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (HomologicalComplex.Hom.f (P (q + 1)) 0)
    (HomologicalComplex.Hom.f (P q) 0)

Tactic:
simp only [P_f_0_eq]

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq