-- 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
x : (f j).ι
y : (f j').ι
⊢ 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)
have 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).ι)) sorry =
            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).ι)) sorry =
                y then
            eqToHom sorry
          else 0
        else 0
      else 0
    else 0)
  ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp,
                eqToHom_trans]