[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ underlying.obj (objX X (n + 1 + 1)) ⟶ underlying.obj (objX X (n + 1))
[PROOFSTEP]
refine'
  factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3)))
    _
      -- We now need to show that it factors!
          -- A morphism factors through an intersection of subobjects if it factors through each.
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ Factors (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
[PROOFSTEP]
refine'
  (finset_inf_factors _).mpr fun i _ =>
    _
      -- A morphism `f` factors through the kernel of `g` exactly if `f ≫ g = 0`.
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
[PROOFSTEP]
apply kernelSubobject_factors
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0) ≫ SimplicialObject.δ X (Fin.succ i) = 0
[PROOFSTEP]
dsimp [objX]
  -- Use a simplicial identity
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0) ≫
      SimplicialObject.δ X (Fin.succ i) =
    0
[PROOFSTEP]
erw [Category.assoc, ← X.δ_comp_δ (Fin.zero_le i.succ)]
  -- We can rewrite the arrow out of the intersection of all the kernels as a composition
      -- of a morphism we don't care about with the arrow out of the kernel of `X.δ i.succ.succ`.
[GOAL]
case w
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ (Fin.succ i)) ≫ SimplicialObject.δ X 0 =
    0
[PROOFSTEP]
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.8376, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (Nat.add n 0 + 1)
x✝ : i ∈ Finset.univ
⊢ Fin.succ i ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ objD X (Nat.zero + 1) ≫ objD X Nat.zero = 0
[PROOFSTEP]
dsimp [objD]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (Nat.succ n + 1) ≫ objD X (Nat.succ n) = 0
[PROOFSTEP]
dsimp [objD]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0 ≫ inv (arrow ⊤) =
    0
[PROOFSTEP]
erw [Subobject.factorThru_arrow_assoc, Category.assoc, ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)), ←
  factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 0 ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
[PROOFSTEP]
erw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc, ←
  X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))), ←
  factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)), Category.assoc,
  kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ 0 ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ Factors (objX Y Nat.zero) (arrow (objX X Nat.zero) ≫ NatTrans.app f (op (SimplexCategory.mk Nat.zero)))
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ Factors (objX Y (Nat.succ n✝)) (arrow (objX X (Nat.succ n✝)) ≫ NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ Factors ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
[PROOFSTEP]
apply top_factors
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
    (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
[PROOFSTEP]
refine' (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ _
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝)))) ≫
      SimplicialObject.δ Y (Fin.succ i) =
    0
[PROOFSTEP]
erw [Category.assoc, ← f.naturality, ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ i ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (n + 1) ≫
      objD Y n =
    objD X n ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        n
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.zero + 1) ≫
      objD Y Nat.zero =
    objD X Nat.zero ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        Nat.zero
[PROOFSTEP]
dsimp [objD, objX]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.succ n✝ + 1) ≫
      objD Y (Nat.succ n✝) =
    objD X (Nat.succ n✝) ≫
      (fun n =>
          factorThru (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))
            (_ : Factors (objX Y n) (arrow (objX X n) ≫ NatTrans.app f (op (SimplexCategory.mk n)))))
        (Nat.succ n✝)
[PROOFSTEP]
dsimp [objD, objX]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (0 + 1))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ 0))))) ≫
      arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k))) ≫
        SimplicialObject.δ Y 0 ≫ inv (arrow ⊤) =
    (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        SimplicialObject.δ X 0 ≫ inv (arrow ⊤)) ≫
      factorThru ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
        (_ : Factors ⊤ (arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0))))
[PROOFSTEP]
aesop_cat
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.84232, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝ + 1))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ (Nat.succ n✝)))))) ≫
      factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k))) ≫
          SimplicialObject.δ Y 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (objX Y (n✝ + 1 + 1)) ≫ SimplicialObject.δ Y 0)) =
    factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n✝ + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
        (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y (Fin.succ k)))
            (arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
              NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝)))))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ { obj := obj, map := fun {X Y} f => map f }.map (𝟙 X) = 𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (𝟙 X)) Nat.zero =
    HomologicalComplex.Hom.f (𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (𝟙 X)) (Nat.succ n✝) =
    HomologicalComplex.Hom.f (𝟙 ({ obj := obj, map := fun {X Y} f => map f }.obj X)) (Nat.succ n✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ 𝟙 (X.obj (op (SimplexCategory.mk 0))))
      (_ : Subobject.Factors (objX X 0) (Subobject.arrow (objX X 0) ≫ NatTrans.app (𝟙 X) (op (SimplexCategory.mk 0)))) =
    𝟙 (Subobject.underlying.obj ⊤)
[PROOFSTEP]
aesop_cat
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n✝ : ℕ
⊢ Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
      (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
        𝟙 (X.obj (op (SimplexCategory.mk (Nat.succ n✝)))))
      (_ :
        Subobject.Factors (objX X (Nat.succ n✝))
          (Subobject.arrow (objX X (Nat.succ n✝)) ≫ NatTrans.app (𝟙 X) (op (SimplexCategory.mk (Nat.succ n✝))))) =
    𝟙 (Subobject.underlying.obj (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := obj, map := fun {X Y} f => map f }.map (f ≫ g) =
    { obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) Nat.zero =
    HomologicalComplex.Hom.f
      ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g) Nat.zero
[PROOFSTEP]
apply Subobject.eq_of_comp_arrow_eq
[GOAL]
case h.succ
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) (Nat.succ n✝) =
    HomologicalComplex.Hom.f
      ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
      (Nat.succ n✝)
[PROOFSTEP]
apply Subobject.eq_of_comp_arrow_eq
[GOAL]
case h.zero.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) Nat.zero ≫
      Subobject.arrow (objX Z✝ Nat.zero) =
    HomologicalComplex.Hom.f
        ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
        Nat.zero ≫
      Subobject.arrow (objX Z✝ Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case h.succ.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ HomologicalComplex.Hom.f ({ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g)) (Nat.succ n✝) ≫
      Subobject.arrow (objX Z✝ (Nat.succ n✝)) =
    HomologicalComplex.Hom.f
        ({ obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g)
        (Nat.succ n✝) ≫
      Subobject.arrow (objX Z✝ (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case h.zero.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Subobject.factorThru ⊤
        (Subobject.arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)) ≫ NatTrans.app g (op (SimplexCategory.mk 0)))
        (_ :
          Subobject.Factors (objX Z✝ 0)
            (Subobject.arrow (objX X✝ 0) ≫ NatTrans.app (f ≫ g) (op (SimplexCategory.mk 0)))) ≫
      Subobject.arrow ⊤ =
    (Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ NatTrans.app f (op (SimplexCategory.mk 0)))
          (_ :
            Subobject.Factors (objX Y✝ 0) (Subobject.arrow (objX X✝ 0) ≫ NatTrans.app f (op (SimplexCategory.mk 0)))) ≫
        Subobject.factorThru ⊤ (Subobject.arrow ⊤ ≫ NatTrans.app g (op (SimplexCategory.mk 0)))
          (_ :
            Subobject.Factors (objX Z✝ 0) (Subobject.arrow (objX Y✝ 0) ≫ NatTrans.app g (op (SimplexCategory.mk 0))))) ≫
      Subobject.arrow ⊤
[PROOFSTEP]
aesop_cat
[GOAL]
case h.succ.h
C : Type u_1
inst✝¹ : Category.{?u.127901, u_1} C
inst✝ : Abelian C
X✝ Y✝ Z✝ : SimplicialObject C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
n✝ : ℕ
⊢ Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
        (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X✝ (Fin.succ k))) ≫
          NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))) ≫
            NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝))))
        (_ :
          Subobject.Factors (objX Z✝ (Nat.succ n✝))
            (Subobject.arrow (objX X✝ (Nat.succ n✝)) ≫ NatTrans.app (f ≫ g) (op (SimplexCategory.mk (Nat.succ n✝))))) ≫
      Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k))) =
    (Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y✝ (Fin.succ k)))
          (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X✝ (Fin.succ k))) ≫
            NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))
          (_ :
            Subobject.Factors (objX Y✝ (Nat.succ n✝))
              (Subobject.arrow (objX X✝ (Nat.succ n✝)) ≫ NatTrans.app f (op (SimplexCategory.mk (Nat.succ n✝))))) ≫
        Subobject.factorThru (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
          (Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Y✝ (Fin.succ k))) ≫
            NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝))))
          (_ :
            Subobject.Factors (objX Z✝ (Nat.succ n✝))
              (Subobject.arrow (objX Y✝ (Nat.succ n✝)) ≫ NatTrans.app g (op (SimplexCategory.mk (Nat.succ n✝)))))) ≫
      Subobject.arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ Z✝ (Fin.succ k)))
[PROOFSTEP]
aesop_cat
