-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
H :
  ∀ (x : (f j).ι) (y : (f j').ι),
    Eq.{v₁ + 1} (α := (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
        { ι := (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).ι)) })
        (fun (x : (f j).ι)
            (y :
              ι.{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).ι)) }) ↦
          if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
            if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x then
              eqToHom ⋯
            else 0
          else 0)
        (fun
            (x :
              ι.{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).ι)) })
            (y : (f j').ι) ↦
          if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
            if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y then
              eqToHom ⋯
            else 0
          else 0)
        x y)
      ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} (f j) (f j'))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      { ι := (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).ι)) })
      (fun (x : (f j).ι)
          (y :
            ι.{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).ι)) }) ↦
        if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
          if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x then
            eqToHom ⋯
          else 0
        else 0)
      fun
        (x :
          ι.{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).ι)) })
        (y : (f j').ι) ↦
      if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
        if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y then
          eqToHom ⋯
        else 0
      else 0)
    (if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0)

Tactic:
ext x y