-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    ((arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
zero₁ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
zero₂ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫
      X.δ (Fin.castSucc 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
zero₃ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫
      X.δ (Fin.succ 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
have zero₄ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  (CategoryStruct.comp (Y :=
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying (kernelSubobject (X.δ (Fin.succ 0))))
      (factorThru (kernelSubobject (X.δ (Fin.succ 0)))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ))) sorry)
      (arrow (kernelSubobject (X.δ (Fin.succ 0)))) ≫
    X.δ (Fin.succ 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
  0
Tactic: rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← 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]