-- 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').ι
⊢ Eq.{v₁ + 1} (α :=
    (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'))
    ((∑ j : Fin n,
          CategoryStruct.comp.{v₁, max 1 u₁} (Y := f j)
            (fun (x : (j : Fin n) × (f j).ι) (y : (f j).ι) ↦
              if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
                if h' :
                    Eq.rec (motive := fun (x_1 : Fin n) (x : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = x_1) ↦ (f x_1).ι)
                        (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                      y then
                  eqToHom ⋯
                else 0
              else 0)
            fun (x : (f j).ι) (y : (j : Fin n) × (f j).ι) ↦
            if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
              if h' :
                  Eq.rec (motive := fun (x : Fin n) (x_1 : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                      (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                    x then
                eqToHom ⋯
              else 0
            else 0)
        (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'))
    (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 : Eq.{v₁ + 1} (α :=
  (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'))
  (∑ c : Fin n,
      CategoryStruct.comp.{v₁, max 1 u₁} (Y := f c)
        (fun (x : (j : Fin n) × (f j).ι) (y : (f c).ι) ↦
          if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = c then
            if h' :
                Eq.rec (motive := fun (x_1 : Fin n) (x : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = x_1) ↦ (f x_1).ι)
                    (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                  y then
              eqToHom sorry
            else 0
          else 0)
        (fun (x : (f c).ι) (y : (j : Fin n) × (f j).ι) ↦
          if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = c then
            if h' :
                Eq.rec (motive := fun (x : Fin n) (x_1 : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                    (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                  x then
              eqToHom sorry
            else 0
          else 0)
        (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'))
  (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'))
Tactic: rw [Finset.sum_apply, Finset.sum_apply]