-- 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
x : (f j).ι
y : (f j').ι
H :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ x_1 : (j : Fin n) × (f j).ι,
      if h : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
        if h_1 :
            Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
              x then
          if h_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
            if h_3 :
                Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                    (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
                  y then
              eqToHom ⋯
            else 0
          else 0
        else 0
      else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ x_1 : (j : Fin n) × (f j).ι,
      if h : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
        if h_1 :
            Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
              x then
          if h_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
            if h_3 :
                Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                    (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
                  y then
              CategoryStruct.comp (Y :=
                (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) (eqToHom ⋯)
                (eqToHom ⋯)
            else
              CategoryStruct.comp (Y :=
                (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) (eqToHom ⋯)
                0
          else
            CategoryStruct.comp (Y :=
              (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) (eqToHom ⋯) 0
        else
          if h : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
            if h_2 :
                Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                    (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
                  y then
              CategoryStruct.comp (Y :=
                (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0
                (eqToHom ⋯)
            else
              CategoryStruct.comp (Y :=
                (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0 0
          else
            CategoryStruct.comp (Y :=
              (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0 0
      else
        if h : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
          if h_1 :
              Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                  (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
                y then
            CategoryStruct.comp (Y :=
              (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0 (eqToHom ⋯)
          else
            CategoryStruct.comp (Y :=
              (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0 0
        else
          CategoryStruct.comp (Y :=
            (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) 0 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp,
                eqToHom_trans]

Premises used: ite_self, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, dite_eq_ite, CategoryTheory.eqToHom_trans