-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
H :
  Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f i).X j)
        (if h : i = i then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j then eqToHom ⋯ else 0
        else 0)
        (if h : i' = i then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
        else 0) :
      (f i).X j ⟶ (f i').X j')
    (CategoryStruct.id.{v₁, max 1 u₁}
        { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
          X := fun (p : (j : Fin n) × (f j).ι) ↦
            (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j') :
      (fun
            (i j :
              ι.{u₁} (C := C)
                { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                  X := fun (p : (j : Fin n) × (f j).ι) ↦
                    (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }) ↦
          Quiver.Hom.{v₁, u₁}
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) :
                Mat_ C }
              i)
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
              j))
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j'))
H₁ :
  ∀ (b : (f i).ι),
    Membership.mem (γ := Finset (f i).ι) Finset.univ b →
      b ≠ j →
        Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
          (CategoryStruct.comp (Y := (f i).X b)
            (if h : i = i then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = b then eqToHom ⋯ else 0
            else 0)
            (if h : i' = i then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = b then eqToHom ⋯ else 0
            else 0))
          0
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (∑ j_1 : (f i).ι,
        CategoryStruct.comp (Y := (f i).X j_1)
          (if h : i = i then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j_1 then eqToHom ⋯ else 0
          else 0)
          (if h : i' = i then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j_1 then eqToHom ⋯ else 0
          else 0) :
      (f i).X j ⟶ (f i').X j')
    (CategoryStruct.id.{v₁, max 1 u₁}
        { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
          X := fun (p : (j : Fin n) × (f j).ι) ↦
            (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j') :
      (fun
            (i j :
              ι.{u₁} (C := C)
                { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                  X := fun (p : (j : Fin n) × (f j).ι) ↦
                    (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }) ↦
          Quiver.Hom.{v₁, u₁}
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) :
                Mat_ C }
              i)
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
              j))
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j'))
have H₂ : j ∉ Finset.univ →
  Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f i).X j)
      (if h : i = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j then eqToHom sorry else 0
      else 0)
      (if h : i' = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom sorry else 0
      else 0))
    0
Tactic: rw [Finset.sum_eq_single j]