[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ HomologicalComplex.Hom.f (AlgebraicTopology.inclusionOfMooreComplexMap X) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
[PROOFSTEP]
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
[PROOFSTEP]
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j (by simp only [Finset.mem_univ])), assoc,
  kernelSubobject_arrow_comp, comp_zero]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ j ∈ Finset.univ
[PROOFSTEP]
simp only [Finset.mem_univ]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ Factors (NormalizedMooreComplex.objX X Nat.zero) (HomologicalComplex.Hom.f PInfty Nat.zero)
[PROOFSTEP]
apply top_factors
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X (Nat.succ n)) (HomologicalComplex.Hom.f PInfty (Nat.succ n))
[PROOFSTEP]
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    i ∈ Finset.univ →
      Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i)))
        (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
[PROOFSTEP]
intro i _
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
[PROOFSTEP]
apply kernelSubobject_factors
[GOAL]
case succ.w
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) ≫ SimplicialObject.δ X (Fin.succ i) = 0
[PROOFSTEP]
exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.88673, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (fun n =>
          factorThru (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
            (_ : Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)))
        (n + 1) ≫
      NormalizedMooreComplex.objD X n =
    AlternatingFaceMapComplex.objD X n ≫
      (fun n =>
          factorThru (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
            (_ : Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)))
        n
[PROOFSTEP]
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow, ←
  inclusionOfMooreComplexMap_f, ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
  inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, ← alternatingFaceMapComplex_obj_d]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.88673, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ HomologicalComplex.d ((alternatingFaceMapComplex A).obj X) (n + 1) n =
    HomologicalComplex.d ((alternatingFaceMapComplex A).obj X) (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
exact PInfty.comm (n + 1) n
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
    PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X
[PROOFSTEP]
ext (_ | n)
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) Nat.zero =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 ≫ 𝟙 (X.obj (Opposite.op (SimplexCategory.mk 0))) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0
[PROOFSTEP]
simp only [comp_id]
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (Nat.succ n) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (Nat.succ n)
[PROOFSTEP]
exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
⊢ x✝¹ = x✝
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n = HomologicalComplex.Hom.f x✝ n
[PROOFSTEP]
dsimp
[GOAL]
case h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n = HomologicalComplex.Hom.f x✝ n
[PROOFSTEP]
ext
[GOAL]
case h.h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n ≫ arrow (NormalizedMooreComplex.objX X n) =
    HomologicalComplex.Hom.f x✝ n ≫ arrow (NormalizedMooreComplex.objX X n)
[PROOFSTEP]
exact HomologicalComplex.congr_hom hf n
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.109759, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInftyToNormalizedMooreComplex X = 𝟙 ((normalizedMooreComplex A).obj X)
[PROOFSTEP]
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
  PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X =
    (N₁.obj X).p ≫
      PInftyToNormalizedMooreComplex X ≫ ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p
[PROOFSTEP]
erw [comp_id, PInfty_comp_PInftyToNormalizedMooreComplex]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ N₁.map f ≫ (fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) Y =
    (fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) X ≫
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f
[PROOFSTEP]
simp only [Functor.comp_map, normalizedMooreComplex_map, PInftyToNormalizedMooreComplex_naturality, Karoubi.hom_ext_iff,
  Karoubi.comp_f, N₁_map_f, PInfty_comp_PInftyToNormalizedMooreComplex_assoc, toKaroubi_map_f, assoc]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X =
    ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p ≫ inclusionOfMooreComplexMap X ≫ (N₁.obj X).p
[PROOFSTEP]
erw [inclusionOfMooreComplexMap_comp_PInfty, id_comp]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f ≫
      (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) Y =
    (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) X ≫ N₁.map f
[PROOFSTEP]
ext
[GOAL]
case h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
i✝ : ℕ
⊢ HomologicalComplex.Hom.f
      ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f ≫
          (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) Y).f
      i✝ =
    HomologicalComplex.Hom.f ((fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) X ≫ N₁.map f).f i✝
[PROOFSTEP]
simp only [Functor.comp_map, normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f, HomologicalComplex.comp_f,
  NormalizedMooreComplex.map_f, inclusionOfMooreComplexMap_f, factorThru_arrow, N₁_map_f,
  inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.map_f]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ((NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) ≫
      NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) =
    𝟙 N₁
[PROOFSTEP]
ext X : 3
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
        ((NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) ≫
          NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X))
        X).f =
    (NatTrans.app (𝟙 N₁) X).f
[PROOFSTEP]
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p,
  NatTrans.id_app, Karoubi.id_eq]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
      NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) =
    𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))
[PROOFSTEP]
ext X : 3
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
        ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
          NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X))
        X).f =
    (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))) X).f
[PROOFSTEP]
rw [← cancel_mono (inclusionOfMooreComplexMap X)]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
          ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
            NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X))
          X).f ≫
      inclusionOfMooreComplexMap X =
    (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))) X).f ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_eq,
  PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X =
    ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
dsimp only [Functor.comp_obj, toKaroubi]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X = 𝟙 ((normalizedMooreComplex A).obj X) ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
erw [id_comp]
