-- 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
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C)
      (Bicone.pt.{0, v₁, max 1 u₁} (J := Fin n) (F := f)
        {
          pt :=
            { ι := (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 (j : Fin n)
              (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,
          ι :=
            fun (j : Fin n) (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,
          ι_π := ⋯ })
      (Bicone.pt.{0, v₁, max 1 u₁} (J := Fin n) (F := f)
        {
          pt :=
            { ι := (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 (j : Fin n)
              (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,
          ι :=
            fun (j : Fin n) (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,
          ι_π := ⋯ }))
    (∑ j : Fin n,
      CategoryStruct.comp.{v₁, max 1 u₁}
        (Bicone.π.{0, v₁, max 1 u₁}
          {
            pt :=
              { ι := (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).ι)) :
                Mat_ C },
            π :=
              fun (j : Fin n)
                (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).ι)) :
                      Mat_ C })
                (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,
            ι :=
              fun (j : Fin n) (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).ι)) :
                      Mat_ C }) ↦
              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,
            ι_π := ⋯ : Bicone.{0, v₁, max 1 u₁} f }
          j)
        (Bicone.ι.{0, v₁, max 1 u₁}
          {
            pt :=
              { ι := (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 (j : Fin n)
                (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,
            ι :=
              fun (j : Fin n) (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,
            ι_π := ⋯ }
          j))
    (CategoryStruct.id.{v₁, max 1 u₁}
      (Bicone.pt.{0, v₁, max 1 u₁} (J := Fin n) (F := f)
        {
          pt :=
            { ι := (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 (j : Fin n)
              (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,
          ι :=
            fun (j : Fin n) (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,
          ι_π := ⋯ }))
have dsimp : Eq.{v₁ + 1} (α :=
  Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ 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).ι)) }
    { ι := (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).ι)) })
  (∑ j : Fin n,
    CategoryStruct.comp.{v₁, max 1 u₁} (Y := f j)
      (fun (x : (j : Fin n) × (f j).ι) (y : (f j).ι) ↦
        if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
          if h' :
              Eq.rec (motive := fun (x_1 : Fin n) (x : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = x_1) ↦ (f x_1).ι)
                  (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                y then
            eqToHom sorry
          else 0
        else 0)
      fun (x : (f j).ι) (y : (j : Fin n) × (f j).ι) ↦
      if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
        if h' :
            Eq.rec (motive := fun (x : Fin n) (x_1 : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
              x then
          eqToHom sorry
        else 0
      else 0)
  (CategoryStruct.id.{v₁, max 1 u₁}
    { ι := (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).ι)) })
Tactic: dsimp