-- 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)
    (∑ j_1 : (j : Fin n) × (f j).ι,
      CategoryStruct.comp (Y :=
        (f (j_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (j_1.snd (β := fun (j : Fin n) ↦ (f j).ι)))
        (if h : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
          if h' :
              Eq.rec (motive := fun (x : Fin n) (x_1 : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                  (j_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                x then
            eqToHom ⋯
          else 0
        else 0)
        (if h : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
          if h' :
              Eq.rec (motive := fun (x : Fin n) (x_1 : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                  (j_1.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) 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
            CategoryStruct.comp (Y :=
              (f (x_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι))) (eqToHom sorry)
              (eqToHom sorry)
          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 sorry) 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 sorry) 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).ι)) sorry =
                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 sorry)
          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).ι)) sorry =
              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 sorry)
        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₁} sorry else 0) x y)
Tactic: simp_rw [dite_comp, comp_dite]