-- 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
j j' : Fin n
⊢ 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)
have 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 sorry
          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 sorry
          else 0
        else 0)
      x y)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: ext x y