awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
zero : IsIso (X := X _⦋0⦌) (f.app (op ⦋0⦌))
succ : ∀ (n : ℕ) (hn : IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))), IsIso (X := X _⦋n + 1⦌) (f.app (op ⦋n + 1⦌))
⊢ IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))

Tactic:
induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.Hom.f, HomologicalComplex.Hom.f, CategoryTheory.SimplicialObject.σ_naturality, and_self, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, CategoryTheory.Functor.map, AlgebraicTopology.DoldKan.MorphComponents.id_φ, CategoryTheory.IsIso.hom_inv_id_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp, AlgebraicTopology.DoldKan.MorphComponents.preComp_φ, AlgebraicTopology.DoldKan.MorphComponents.preComp, AlgebraicTopology.DoldKan.MorphComponents.postComp_φ, AlgebraicTopology.DoldKan.N₁, AlgebraicTopology.DoldKan.MorphComponents.id, CategoryTheory.inv, OfNat.ofNat, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ))
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
        (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
          Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))

Tactic:
CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
refine_1 :
  ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
    Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
      (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
refine_2 :
  ∀ (P Q : Karoubi (SimplicialObject.{v_1, u_1} C)) (f : P ⟶ Q),
    Eq (α :=
      Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
        (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
        (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) Q))
      (CategoryTheory.Functor.map (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) f)
      (CategoryStruct.comp (Y :=
        Functor.obj
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          P)
        (eqToHom ⋯)
        (CategoryTheory.Functor.map
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            f ≫
          eqToHom ⋯))
⊢ Eq (α := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ))
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
        (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
          Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))

Tactic:
refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)

Tactic:
HomologicalComplex.ext ?_ ?_

Premises used: HomologicalComplex.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
refine_1 :
  HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) =
    HomologicalComplex.X
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
refine_1₁ :
  ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      Eq (α :=
        HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) i ⟶
          HomologicalComplex.X
            (Functor.obj
              (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                  (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                    Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                      (ComplexShape.down ℕ)))
              P)
            j)
        (HomologicalComplex.d (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) i j ≫
          eqToHom ⋯)
        (eqToHom ⋯ ≫
          HomologicalComplex.d
            (Functor.obj
              (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                  (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                    Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                      (ComplexShape.down ℕ)))
              P)
            i j)
⊢ Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)

Tactic:
refine HomologicalComplex.ext ?_ ?_

Premises used: HomologicalComplex.ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
refine_1 :
  ∀ (n : ℕ),
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).X =
      (HomologicalComplex.X
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          n).X
refine_1₁ :
  ∀ (n : ℕ),
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).p ≫
        eqToHom ⋯ =
      eqToHom ⋯ ≫
        (HomologicalComplex.X
            (Functor.obj
              (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                  (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                    Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                      (ComplexShape.down ℕ)))
              P)
            n).p
⊢ HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) =
    HomologicalComplex.X
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).X =
    (HomologicalComplex.X
        (Functor.obj
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          P)
        n).X

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
refine_1 :
  Eq (α := P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n :
            HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n)
          (P.p.app (op ⦋n⦌)) ≫
        𝟙 (P.X _⦋n⦌) :
      P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
    (𝟙 (P.X _⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) : P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
⊢ (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).p ≫
      eqToHom ⋯ =
    eqToHom ⋯ ≫
      (HomologicalComplex.X
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          n).p

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α := P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n :
            HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n)
          (P.p.app (op ⦋n⦌)) ≫
        𝟙 (P.X _⦋n⦌) :
      P.X _⦋n⦌ ⟶ P.X _⦋n⦌)
    (𝟙 (P.X _⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) : P.X _⦋n⦌ ⟶ P.X _⦋n⦌)

Tactic:
simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp]

Premises used: CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.PInfty_f_naturality, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
refine_1 :
  Eq (α :=
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1)).X ⟶
      (HomologicalComplex.X
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.d (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1) n ≫
        eqToHom ⋯))
    (Karoubi.Hom.f
      (eqToHom ⋯ ≫
        HomologicalComplex.d
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          (n + 1) n))
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1) ⟶
      HomologicalComplex.X
        (Functor.obj
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          P)
        n)
    (HomologicalComplex.d (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1) n ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫
      HomologicalComplex.d
        (Functor.obj
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          P)
        (n + 1) n)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n)
    (HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) (n + 1) ≫
      HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
    (HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n ≫
      HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) n)

Tactic:
have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
h :
  Eq (α :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1) ⟶
      HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) n)
    (HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) (n + 1) ≫
      HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
    (HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n ≫
      HomologicalComplex.Hom.f (AlternatingFaceMapComplex.map P.p) n)
refine_1 :
  Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n⦌)
        (CategoryStruct.comp (Y := P.X _⦋n + 1⦌)
            (HomologicalComplex.Hom.f PInfty (n + 1) :
              HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1) ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1))
            (P.p.app (op ⦋n + 1⦌)) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
        (Karoubi.Hom.f (eqToHom ⋯)) :
      P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n + 1⦌) (Karoubi.Hom.f (eqToHom ⋯))
        (CategoryStruct.comp (Y := P.X _⦋n + 1⦌) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty (n + 1)))
          (Karoubi.Hom.f
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n))) :
      P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
⊢ Eq (α :=
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1)).X ⟶
      (HomologicalComplex.X
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.d (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) (n + 1) n ≫
        eqToHom ⋯))
    (Karoubi.Hom.f
      (eqToHom ⋯ ≫
        HomologicalComplex.d
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          (n + 1) n))

Tactic:
dsimp [N₂, karoubiChainComplexEquivalence,
        KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢

Premises used: AlgebraicTopology.DoldKan.N₂, CategoryTheory.Idempotents.karoubiChainComplexEquivalence, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
h :
  Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (P.p.app (op ⦋n + 1⦌) ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
    (HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n ≫ P.p.app (op ⦋n⦌))
⊢ Eq (α := P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n⦌)
        (CategoryStruct.comp (Y := P.X _⦋n + 1⦌)
            (HomologicalComplex.Hom.f PInfty (n + 1) :
              HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1) ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj P.X) (n + 1))
            (P.p.app (op ⦋n + 1⦌)) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n)
        (Karoubi.Hom.f (eqToHom ⋯)) :
      P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
    (CategoryStruct.comp (Y := P.X _⦋n + 1⦌) (Karoubi.Hom.f (eqToHom ⋯))
        (CategoryStruct.comp (Y := P.X _⦋n + 1⦌) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty (n + 1)))
          (Karoubi.Hom.f
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n))) :
      P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)

Tactic:
simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id,
        karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
        ← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]

Premises used: CategoryTheory.Idempotents.app_idem_assoc, CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.eqToHom_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, HomologicalComplex.Hom.comm_assoc, AlgebraicTopology.DoldKan.karoubi_PInfty_f