-- 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
E : Type u_2
inst_4 : Category.{v₁, u_2} E
inst_5 : Preadditive.{v₁, u_2} E
F : Functor.{v₁, v₁, u₁, u_1} C D
inst_6 : F.Additive
G : Functor.{v₁, v₁, u_1, u_2} D E
inst_7 : G.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
H :
  ∀ (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).ι)
    (j :
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι),
    Eq (α :=
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).ι)
            (j :
              (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  N).ι) ↦
          Quiver.Hom.{v₁, u_2} ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  N).X
              j))
        i j)
      (CategoryStruct.comp.{v₁, max 1 u_2} (map.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ f)
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              N))
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι) ↦
            Quiver.Hom.{v₁, u_2} ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).X
                j))
          i j)
      (CategoryStruct.comp.{v₁, max 1 u_2}
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              M))
          (map.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) f)
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι) ↦
            Quiver.Hom.{v₁, u_2} ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).X
                j))
          i j)
H₁ H₂ :
  ∀
    (j :
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι)
    (ι : 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_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι),
    Eq (α :=
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
            (j :
              (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  N).ι) ↦
          Quiver.Hom.{v₁, u_2}
            ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  N).X
              j))
        i j)
      (CategoryStruct.comp.{v₁, max 1 u_2} (map.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ f)
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              N))
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι) ↦
            Quiver.Hom.{v₁, u_2}
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).X
                j))
          i j)
      (CategoryStruct.comp.{v₁, max 1 u_2}
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              { ι := ι, fintype := fintype, X := X }))
          (map.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) f)
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).ι) ↦
            Quiver.Hom.{v₁, u_2}
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N).X
                j))
          i j)
H₃ :
  ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C)
    (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
    (ι_1 : Type) [fintype_1 : Fintype ι_1] (X_1 : ι_1 → C)
    (j :
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
          { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).ι)
    (f :
      Quiver.Hom.{v₁, max 1 u₁} { ι := ι, fintype := fintype, X := X : Mat_ C }
        { ι := ι_1, fintype := fintype_1, X := X_1 }),
    Eq (α :=
      (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
            (j :
              (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).ι) ↦
          Quiver.Hom.{v₁, u_2}
            ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
            ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                  { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).X
              j))
        i j)
      (CategoryStruct.comp.{v₁, max 1 u_2} (map.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ f)
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              { ι := ι_1, fintype := fintype_1, X := X_1 }))
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                    { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).ι) ↦
            Quiver.Hom.{v₁, u_2}
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                    { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).X
                j))
          i j)
      (CategoryStruct.comp.{v₁, max 1 u_2}
          (Iso.hom.{v₁, max 1 u_2}
            ((fun (M : Mat_ C) ↦
                (eqToIso.{v₁, max 1 u_2} ⋯ :
                  Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                    (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                      (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
              { ι := ι, fintype := fintype, X := X }))
          (map.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) f)
          i j :
        (fun (i : (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).ι)
              (j :
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                    { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).ι) ↦
            Quiver.Hom.{v₁, u_2}
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C }).X i)
              ((obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                    (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
                    { ι := ι_1, fintype := fintype_1, X := X_1 : Mat_ C }).X
                j))
          i j)
⊢ Eq (α :=
    Quiver.Hom.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) N))
    (CategoryStruct.comp.{v₁, max 1 u_2} (map.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ f)
      (Iso.hom.{v₁, max 1 u_2}
        ((fun (M : Mat_ C) ↦
            (eqToIso.{v₁, max 1 u_2} ⋯ :
              Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                  (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
          N)))
    (CategoryStruct.comp.{v₁, max 1 u_2}
      (Iso.hom.{v₁, max 1 u_2}
        ((fun (M : Mat_ C) ↦
            (eqToIso.{v₁, max 1 u_2} ⋯ :
              Iso.{v₁, max 1 u_2} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
                (obj.{v₁, v₁, max 1 u₁, max 1 u_2}
                  (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)))
          M))
      (map.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) f))

Tactic:
classical
    ext
    cases M; cases N
    simp [comp_dite, dite_comp]

Premises used: CategoryTheory.dite_comp, CategoryTheory.comp_dite