-- 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
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))) ⋯)
        (arrow (kernelSubobject (X.δ (Fin.succ 0)))) ≫
      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]