awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
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
⊢ 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)
have refine_1₁ : ∀ (n : ℕ),
  (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).p ≫
      eqToHom sorry =
    eqToHom sorry ≫
      (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: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
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).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
have 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⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
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 (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)
have 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 sorry))
  (Karoubi.Hom.f
    (eqToHom sorry ≫
      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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (hypothesis)
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 (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))
have 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)
Tactic: have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
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)
⊢ 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))
have 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 sorry)) :
    P.X _⦋n + 1⦌ ⟶ P.X _⦋n⦌)
  (CategoryStruct.comp (Y := P.X _⦋n + 1⦌) (Karoubi.Hom.f (eqToHom sorry))
      (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: dsimp [N₂, karoubiChainComplexEquivalence,
        KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
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 ⋯))
have refine_2 : ∀ (n : ℕ),
  Eq (α :=
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).X ⟶
      (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) Q) n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) f) n))
    (Karoubi.Hom.f
      (HomologicalComplex.Hom.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 sorry)
          (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 sorry))
        n))
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi (SimplicialObject.{v_1, u_1} C)
f : P ⟶ Q
n : ℕ
⊢ Eq (α :=
    (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).X ⟶
      (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) Q) n).X)
    (Karoubi.Hom.f
      (HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) f) n))
    (Karoubi.Hom.f
      (HomologicalComplex.Hom.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 ⋯))
        n))
have refine_2 : Eq (α := P.X _⦋n⦌ ⟶ Q.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)
      (f.f.app (op ⦋n⦌)) :
    P.X _⦋n⦌ ⟶ Q.X _⦋n⦌)
  (CategoryStruct.comp (Y := P.X _⦋n⦌) (Karoubi.Hom.f (HomologicalComplex.Hom.f (eqToHom sorry) n))
      (CategoryStruct.comp (Y := Q.X _⦋n⦌) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) ≫ f.f.app (op ⦋n⦌))
        (Karoubi.Hom.f (HomologicalComplex.Hom.f (eqToHom sorry) n))) :
    P.X _⦋n⦌ ⟶ Q.X _⦋n⦌)
Tactic: dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A B : Karoubi (SimplicialObject.{v_1, u_1} C)
f : A ⟶ B
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₂ A) (CategoryTheory.Functor.map N₂ f)
F₁ : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi.{v_1, u_1} C) ⥤ Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi.{v_1, u_1} C)) ℕ :=
  Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ)
F₄ : HomologicalComplex (Karoubi (Karoubi.{v_1, u_1} C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)
F : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⥤
  HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) :=
  F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)
have rw : IsIso (C := HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ)) (X :=
  Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) A) (Y :=
  Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) B)
  (CategoryTheory.Functor.map (Equivalence.functor (karoubiChainComplexEquivalence C ℕ))
      (CategoryTheory.Functor.map N₂ f) :
    Quiver.Hom (V := HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ))
      (Functor.obj (Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) (Functor.obj N₂ A))
      (Functor.obj (Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) (Functor.obj N₂ B)))
Tactic: rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A B : Karoubi (SimplicialObject.{v_1, u_1} C)
f : A ⟶ B
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₂ A) (CategoryTheory.Functor.map N₂ f)
F₁ : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi.{v_1, u_1} C) ⥤ Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi.{v_1, u_1} C)) ℕ :=
  Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ)
F₄ : HomologicalComplex (Karoubi (Karoubi.{v_1, u_1} C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) :=
  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)
F : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⥤
  HomologicalComplex (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) :=
  F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso f
have this : IsIso (F.map f)
Tactic: have : IsIso (F.map f) := by
      simp only [F, F₁]
      rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
      apply Functor.map_isIso
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
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 : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
⊢ Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f (AlgebraicTopology.inclusionOfMooreComplexMap X) (n + 1) ≫ X.δ j.succ) 0
have dsimp : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X.obj (Opposite.op { len := n : SimplexCategory }))
  (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ j.succ) 0
Tactic: dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
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 : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ j.succ) 0
have rw : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X.obj (Opposite.op { len := n : SimplexCategory }))
  (((kernelSubobject (X.δ j.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
      (kernelSubobject (X.δ j.succ)).arrow) ≫
    X.δ j.succ)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
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 : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
rw :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (((kernelSubobject (X.δ j.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ j.succ)).arrow) ≫
      X.δ j.succ)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ j.succ) 0
have rw₁ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X.obj (Opposite.op { len := n : SimplexCategory }))
  ((kernelSubobject (X.δ j.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    (kernelSubobject (X.δ j.succ)).arrow ≫ X.δ j.succ)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, comp_zero]