Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋1⦌)) ⋯ ≫
      𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0 ≫ inv ⊤.arrow =
    (𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow) ≫
      ⊤.factorThru (⊤.arrow ≫ f.app (op ⦋0⦌)) ⋯

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0) ⋯
      else 0) =
    (if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯
      else 0) ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯

Tactic:
<;>

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋1⦌)) ⋯ ≫
      𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0 ≫ inv ⊤.arrow =
    (𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow) ≫
      ⊤.factorThru (⊤.arrow ≫ f.app (op ⦋0⦌)) ⋯

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).arrow ≫ Y.δ 0) ⋯
      else 0) =
    (if n✝ + 1 + 1 = n✝ + 1 + 1 then
        𝟙 (underlying.obj (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ))) ≫
          (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
            ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯
      else 0) ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (Y.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯