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
P Q : Karoubi (SimplicialObject.{v_1, u_1} C)
f : P ⟶ Q
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 ⋯)
            (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))
⊢ 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 ⋯))

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 Q : Karoubi (SimplicialObject.{v_1, u_1} C)
f : P ⟶ Q
n : ℕ
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 ⋯) 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 ⋯) n))) :
      P.X _⦋n⦌ ⟶ Q.X _⦋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))

Tactic:
dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]

Premises used: CategoryTheory.Idempotents.KaroubiKaroubi.inverse, CategoryTheory.Functor.mapHomologicalComplex
-- 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 Q : Karoubi (SimplicialObject.{v_1, u_1} C)
f : P ⟶ Q
n : ℕ
⊢ 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 ⋯) 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 ⋯) n))) :
      P.X _⦋n⦌ ⟶ Q.X _⦋n⦌)

Tactic:
simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f,
      assoc, comp_id, PInfty_f_naturality, app_p_comp,
      karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl,
      PInfty_f_naturality_assoc, app_comp_p, PInfty_f_idem_assoc]

Premises used: HomologicalComplex.eqToHom_f, CategoryTheory.Category.assoc, CategoryTheory.Idempotents.app_p_comp, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, CategoryTheory.Idempotents.Karoubi.eqToHom_f, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.app_comp_p, AlgebraicTopology.DoldKan.PInfty_f_naturality, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, AlgebraicTopology.DoldKan.N₂_obj_p_f, AlgebraicTopology.DoldKan.karoubi_PInfty_f
-- 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
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₄
simp : IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)
⊢ IsIso (F.map f)

Tactic:
simp only [F, F₁]
-- 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
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₄
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)))
⊢ IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)

Tactic:
rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]

Premises used: AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CategoryTheory.Functor.comp_map
-- 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
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 (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:
apply Functor.map_isIso

Premises used: CategoryTheory.Functor.map_isIso
-- 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
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.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
-- 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
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₄
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- 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
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₄
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- 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 : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
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
⊢ 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

Tactic:
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]

Premises used: AlgebraicTopology.inclusionOfMooreComplexMap, AlgebraicTopology.NormalizedMooreComplex.objX
-- 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 : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
⊢ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ j

Tactic:
simp
-- 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 : ℕ
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
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
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))) ⋯ ≫
      0)
    0
rw₃ rw₄ :
  Eq.{v_1 + 1} (α :=
    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 }))
    0 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

Tactic:
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, Finset.univ, CategoryTheory.Limits.comp_zero, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Subobject.finset_inf_arrow_factors, CategoryTheory.Limits.kernelSubobject_arrow_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
n : ℕ
zero : Factors (X := HomologicalComplex.X K[X] 0) (NormalizedMooreComplex.objX X 0) (HomologicalComplex.Hom.f PInfty 0)
succ :
  ∀ (n : ℕ),
    Factors (X := HomologicalComplex.X K[X] (n + 1)) (NormalizedMooreComplex.objX X (n + 1))
      (HomologicalComplex.Hom.f PInfty (n + 1))
⊢ (NormalizedMooreComplex.objX X n).Factors (X := HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)

Tactic:
rcases n with _ | 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
⊢ Factors (X := HomologicalComplex.X K[X] 0) (NormalizedMooreComplex.objX X 0) (HomologicalComplex.Hom.f PInfty 0)

Tactic:
apply top_factors

Premises used: CategoryTheory.Subobject.top_factors
-- 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 : ℕ
succ :
  ∀ (i : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
      (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
        (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))
⊢ Factors (X := HomologicalComplex.X K[X] (n + 1)) (NormalizedMooreComplex.objX X (n + 1))
    (HomologicalComplex.Hom.f PInfty (n + 1))

Tactic:
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]

Premises used: AlgebraicTopology.DoldKan.PInfty_f, CategoryTheory.Subobject.finset_inf_factors, AlgebraicTopology.NormalizedMooreComplex.objX
-- 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 : ℕ
i : Fin (n + 1)
succ :
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))
⊢ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))

Tactic:
_
-- 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 : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ X.δ i.succ) 0
⊢ (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))

Tactic:
apply kernelSubobject_factors

Premises used: CategoryTheory.Limits.kernelSubobject_factors
-- 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 : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
    (HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ X.δ i.succ) 0

Tactic:
(HigherFacesVanish.of_P (n + 1) n) i le_add_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, HAdd.hAdd, OfNat.ofNat, le_add_self