awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_4 : F.Additive
M : Mat_ C
i : M.ι
dsimp :
  Eq (α := F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i)
        (CategoryStruct.comp (Y :=
          F.obj (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
          (biproduct.desc fun (j : M.ι) ↦
            F.map
              (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
                (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j))
          (F.map
            (biproduct.desc.{0, v₁, max 1 u₁} fun (i : M.ι) (x : PUnit.{1}) (k : M.ι) ↦
              if h : i = k then eqToHom ⋯ else 0))) :
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
    (F.map
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
          biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
          (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
            (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i)
          (biproduct.desc.{0, v₁, max 1 u₁} fun (i : M.ι) (x : PUnit.{1}) (k : M.ι) ↦
            if h : i = k then eqToHom ⋯ else 0)) :
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
⊢ CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i :
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶
          biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (Iso.inv (additiveObjIsoBiproduct F M) :
        (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
          F.obj M) =
    F.map
      (CategoryStruct.comp.{v₁, max 1 u₁}
        (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
          (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i)
        (Iso.inv.{v₁, max 1 u₁} M.isoBiproductEmbedding))

Tactic:
dsimp [additiveObjIsoBiproduct, Functor.mapBiproduct, Functor.mapBicone]

Premises used: CategoryTheory.Functor.mapBicone, CategoryTheory.Mat_.additiveObjIsoBiproduct, CategoryTheory.Functor.mapBiproduct
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_4 : F.Additive
M : Mat_ C
i : M.ι
⊢ Eq (α := F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i)
        (CategoryStruct.comp (Y :=
          F.obj (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
          (biproduct.desc fun (j : M.ι) ↦
            F.map
              (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
                (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j))
          (F.map
            (biproduct.desc.{0, v₁, max 1 u₁} fun (i : M.ι) (x : PUnit.{1}) (k : M.ι) ↦
              if h : i = k then eqToHom ⋯ else 0))) :
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
    (F.map
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
          biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
          (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
            (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i)
          (biproduct.desc.{0, v₁, max 1 u₁} fun (i : M.ι) (x : PUnit.{1}) (k : M.ι) ↦
            if h : i = k then eqToHom ⋯ else 0)) :
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)

Tactic:
simp only [biproduct.ι_desc, biproduct.ι_desc_assoc, ← F.map_comp]

Premises used: CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biproduct.ι_desc_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
w :
  ∀ (j : M.ι),
    Eq (α :=
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
            (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j :
          F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
            biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
        (Iso.inv (additiveObjIsoBiproduct F M) ≫
            F.map f ≫ F.map fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
          (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
            F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))))
      (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j)
        (biproduct.desc fun (j : M.ι) ↦ F.map (Functor.map (embedding C) (f j i))))
⊢ Eq (α :=
    (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (Iso.inv (additiveObjIsoBiproduct F M) ≫
        F.map f ≫ F.map fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (biproduct.desc fun (j : M.ι) ↦ F.map (Functor.map (embedding C) (f j i)) :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))

Tactic:
ext j : 1
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
j : M.ι
w :
  Eq (α :=
    F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (F.map
      (CategoryStruct.comp.{v₁, max 1 u₁}
        (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
        (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)))
    (F.map (Functor.map (embedding C) (f j i)))
⊢ Eq (α :=
    F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j :
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
          biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (Iso.inv (additiveObjIsoBiproduct F M) ≫
          F.map f ≫ F.map fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
        (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
          F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))))
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.ι.{0, v₁, u₁} (C := D)
        (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j)
      (biproduct.desc fun (j : M.ι) ↦ F.map (Functor.map (embedding C) (f j i))))

Tactic:
simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
    biproduct.ι_desc, ← F.map_comp]

Premises used: CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc, CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Mat_.isoBiproductEmbedding_inv, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
j : M.ι
w :
  Eq (α :=
    Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
      (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁}
      (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
        if h : j = k then eqToHom ⋯ else 0)
      (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
    (Functor.map (embedding C) (f j i))
⊢ Eq (α :=
    F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (F.map
      (CategoryStruct.comp.{v₁, max 1 u₁}
        (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
        (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)))
    (F.map (Functor.map (embedding C) (f j i)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
j : M.ι
w :
  Eq (α :=
    (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
          (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
        Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
          ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
      PUnit.unit PUnit.unit)
    (CategoryStruct.comp.{v₁, max 1 u₁}
        (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
        (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
        PUnit.unit PUnit.unit :
      (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
            (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
          Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
            ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
        PUnit.unit PUnit.unit)
    (Functor.map (embedding C) (f j i) PUnit.unit PUnit.unit :
      (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
            (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
          Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
            ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
        PUnit.unit PUnit.unit)
⊢ Eq (α :=
    Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
      (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁}
      (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
        if h : j = k then eqToHom ⋯ else 0)
      (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
    (Functor.map (embedding C) (f j i))

Tactic:
funext ⟨⟩ ⟨⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
j : M.ι
⊢ Eq (α :=
    (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
          (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
        Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
          ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
      PUnit.unit PUnit.unit)
    (CategoryStruct.comp.{v₁, max 1 u₁}
        (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
        (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
        PUnit.unit PUnit.unit :
      (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
            (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
          Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
            ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
        PUnit.unit PUnit.unit)
    (Functor.map (embedding C) (f j i) PUnit.unit PUnit.unit :
      (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
            (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
          Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
            ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
        PUnit.unit PUnit.unit)

Tactic:
simp [comp_apply, dite_comp, comp_dite]

Premises used: CategoryTheory.dite_comp, CategoryTheory.Mat_.comp_apply, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
w :
  ∀ (i j : X.ι),
    Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
          (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
            (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
              Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
                (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
            (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
        F.obj (X.X j) ⟶ F.obj (X.X i))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
          (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
        F.obj (X.X j) ⟶ F.obj (X.X i))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
      (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
    (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
      Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
    (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) :
      Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))

Tactic:
ext i j
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
i j : X.ι
h : j = i
pos :
  Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X j))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) j :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X j))) :
      F.obj (X.X j) ⟶ F.obj (X.X j))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) j) :
      F.obj (X.X j) ⟶ F.obj (X.X j))
⊢ Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
      F.obj (X.X j) ⟶ F.obj (X.X i))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
j : X.ι
⊢ Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X j))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) j :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X j))) :
      F.obj (X.X j) ⟶ F.obj (X.X j))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) j) :
      F.obj (X.X j) ⟶ F.obj (X.X j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
i j : X.ι
h : ¬j = i
⊢ Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
      F.obj (X.X j) ⟶ F.obj (X.X i))

Tactic:
simp [h]