-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
H :
  ∀ (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)
⊢ Eq (α :=
    Quiver.Hom.{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)) N))
    (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)))
    (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))

Tactic:
ext