-- 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
n : ℕ
succ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
      (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
        arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
      ⋯)
    0
succ₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n + 1⦌)
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
    0
succ₂ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n + 1⦌)
    ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0) 0
succ₃ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n + 1⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ X.δ 0) 0
succ₄ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n + 1⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫
      X.δ (Fin.castSucc 0) ≫ X.δ 0)
    0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯)
    0
have succ₅ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X _⦋n + 1⦌)
  (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ (Fin.succ 0) ≫ X.δ 0) 0
Tactic: rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
      ← Fin.castSucc_zero,
      ← 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]