-- 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
D : Type u_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).ι
j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι
⊢ Eq (α :=
    (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).ι)
          (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
        Quiver.Hom.{v₁, u₁} ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).X i)
          ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
      i j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (map.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) f)
        (Iso.hom.{v₁, max 1 u₁}
          ((fun (M : Mat_ C) ↦
              (eqToIso.{v₁, max 1 u₁} ⋯ :
                Iso.{v₁, max 1 u₁} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M)
                  (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) M)))
            N))
        i j :
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).ι)
            (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
          Quiver.Hom.{v₁, u₁} ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
        i j)
    (CategoryStruct.comp.{v₁, max 1 u₁}
        (Iso.hom.{v₁, max 1 u₁}
          ((fun (M : Mat_ C) ↦
              (eqToIso.{v₁, max 1 u₁} ⋯ :
                Iso.{v₁, max 1 u₁} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M)
                  (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) M)))
            M))
        (map.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) f) i j :
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).ι)
            (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
          Quiver.Hom.{v₁, u₁} ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
        i j)
have H : ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C)
  (f : Quiver.Hom.{v₁, max 1 u₁} { ι := ι, fintype := fintype, X := X : Mat_ C } N)
  (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).ι),
  Eq (α :=
    (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
          (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
        Quiver.Hom.{v₁, u₁}
          ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
          ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
      i j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (map.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) f)
        (Iso.hom.{v₁, max 1 u₁}
          ((fun (M : Mat_ C) ↦
              (eqToIso.{v₁, max 1 u₁} sorry :
                Iso.{v₁, max 1 u₁} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M)
                  (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) M)))
            N))
        i j :
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
            (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
          Quiver.Hom.{v₁, u₁}
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
        i j)
    (CategoryStruct.comp.{v₁, max 1 u₁}
        (Iso.hom.{v₁, max 1 u₁}
          ((fun (M : Mat_ C) ↦
              (eqToIso.{v₁, max 1 u₁} sorry :
                Iso.{v₁, max 1 u₁} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M)
                  (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) M)))
            { ι := ι, fintype := fintype, X := X }))
        (map.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) f) i j :
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
            (j : (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).ι) ↦
          Quiver.Hom.{v₁, u₁}
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) N).X j))
        i j)
Tactic: cases M
Cleared hypotheses: M, f, i