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
M : Mat_ C
i j b : M.ι
h_1 : Membership.mem (γ := Finset M.ι) Finset.univ b
hb : b ≠ i
h :
  Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (∑ j_1 : PUnit.{1},
      CategoryStruct.comp (Y := M.X b) (if h : i = b then eqToHom ⋯ else 0) (if h : b = j then eqToHom ⋯ else 0))
    0
⊢ Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X b))
      (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = b then eqToHom ⋯ else 0)
      (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : b = k then eqToHom ⋯ else 0) i j)
    0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j b : M.ι
h_1 : Membership.mem (γ := Finset M.ι) Finset.univ b
hb : b ≠ i
h :
  Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (∑ j_1 ∈ {PUnit.unit},
      CategoryStruct.comp (Y := M.X b) (if h : i = b then eqToHom ⋯ else 0) (if h : b = j then eqToHom ⋯ else 0))
    0
h₁ :
  Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (CategoryStruct.comp (Y := M.X b) (if h : i = b then eqToHom ⋯ else 0) (if h : b = j then eqToHom ⋯ else 0)) 0
h₂ : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j) (CategoryStruct.comp (Y := M.X b) 0 (if h : b = j then eqToHom ⋯ else 0)) 0
h₃ h₄ : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j) 0 0
⊢ Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (∑ j_1 : PUnit.{1},
      CategoryStruct.comp (Y := M.X b) (if h : i = b then eqToHom ⋯ else 0) (if h : b = j then eqToHom ⋯ else 0))
    0

Tactic:
rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_comp]

Premises used: Ne.symm, dif_neg, Finset.sum_singleton, CategoryTheory.Limits.zero_comp, Fintype.univ_ofSubsingleton
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
h : i ∉ Finset.univ
⊢ Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
      (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom ⋯ else 0) i j)
    0

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
⊢ Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
      (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom ⋯ else 0) i j)
    (if h : i = j then eqToHom ⋯ else 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
w :
  ∀ (j : M.ι),
    Eq.{v₁ + 1} (α :=
      Quiver.Hom.{v₁, max 1 u₁}
        (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
        (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)))
      (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))
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
          (biproduct.desc.{0, v₁, max 1 u₁}
            fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
            if h : i = k then eqToHom ⋯ else 0)
          (biproduct.lift.{0, v₁, max 1 u₁}
            fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
            if h : j = i then eqToHom ⋯ else 0))
        (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j))
      (CategoryStruct.comp.{v₁, max 1 u₁}
        (CategoryStruct.id.{v₁, max 1 u₁}
          (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₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C)
      (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₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
      (biproduct.desc.{0, v₁, max 1 u₁}
        fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
        if h : i = k then eqToHom ⋯ else 0)
      (biproduct.lift.{0, v₁, max 1 u₁}
        fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
        if h : j = i then eqToHom ⋯ else 0))
    (CategoryStruct.id.{v₁, max 1 u₁}
      (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))

Tactic:
apply biproduct.hom_ext

Premises used: CategoryTheory.Limits.biproduct.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
w :
  Eq.{v₁ + 1} (α :=
    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) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
      (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)
      fun (j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
      if h : j = i then eqToHom ⋯ else 0)
    (if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0)
⊢ Eq.{v₁ + 1} (α :=
    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) (M.X i)))
    (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)) j)
        (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))
          (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
            (biproduct.desc.{0, v₁, max 1 u₁}
              fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
              if h : i = k then eqToHom ⋯ else 0)
            (biproduct.lift.{0, v₁, max 1 u₁}
              fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
              if h : j = i then eqToHom ⋯ else 0))
          (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      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) (M.X i)))
    (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)) j)
        (CategoryStruct.comp.{v₁, max 1 u₁}
          (CategoryStruct.id.{v₁, max 1 u₁}
            (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₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      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) (M.X i)))

Tactic:
simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc,
      biproduct.ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.ι_desc_assoc, CategoryTheory.Limits.biproduct.lift_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
w :
  Eq.{v₁ + 1} (α :=
    (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) (M.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) (M.X i)).X j_1))
      PUnit.unit PUnit.unit)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
      (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)
      (fun (j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
        if h : j = i then eqToHom ⋯ else 0)
      PUnit.unit PUnit.unit)
    ((if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0) PUnit.unit PUnit.unit)
⊢ Eq.{v₁ + 1} (α :=
    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) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
      (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)
      fun (j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
      if h : j = i then eqToHom ⋯ else 0)
    (if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0)

Tactic:
ext ⟨⟩ ⟨⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
w :
  Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (if h : j = i then eqToHom ⋯ else 0)
    ((if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0) PUnit.unit PUnit.unit)
⊢ Eq.{v₁ + 1} (α :=
    (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) (M.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) (M.X i)).X j_1))
      PUnit.unit PUnit.unit)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
      (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)
      (fun (j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
        if h : j = i then eqToHom ⋯ else 0)
      PUnit.unit PUnit.unit)
    ((if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0) PUnit.unit PUnit.unit)

Tactic:
simp only [embedding, comp_apply, comp_dite, dite_comp, comp_zero, zero_comp,
      Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]

Premises used: Finset.mem_univ, CategoryTheory.Limits.comp_zero, CategoryTheory.dite_comp, CategoryTheory.eqToHom_refl, ite_true, Finset.sum_dite_eq', CategoryTheory.Category.comp_id, CategoryTheory.Mat_.embedding, CategoryTheory.Mat_.comp_apply, CategoryTheory.Limits.zero_comp, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
pos : ∀ (h : j = i), Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (eqToHom ⋯) (eqToHom.{v₁, max 1 u₁} ⋯ PUnit.unit PUnit.unit)
neg : ∀ (h : ¬j = i), Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) 0 (0 PUnit.unit PUnit.unit)
⊢ Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (if h : j = i then eqToHom ⋯ else 0)
    ((if h : j = i then eqToHom.{v₁, max 1 u₁} ⋯ else 0) PUnit.unit PUnit.unit)

Tactic:
split_ifs with h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
h : j = i
pos : Eq.{v₁ + 1} (α := M.X j ⟶ M.X j) (eqToHom ⋯) (eqToHom.{v₁, max 1 u₁} ⋯ PUnit.unit PUnit.unit)
⊢ Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (eqToHom ⋯) (eqToHom.{v₁, max 1 u₁} ⋯ PUnit.unit PUnit.unit)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
j : M.ι
⊢ Eq.{v₁ + 1} (α := M.X j ⟶ M.X j) (eqToHom ⋯) (eqToHom.{v₁, max 1 u₁} ⋯ PUnit.unit PUnit.unit)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
h : ¬j = i
⊢ Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) 0 (0 PUnit.unit PUnit.unit)

Tactic:
rfl
-- 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
⊢ HasBiproduct.{0, v₁, u₁} (C := D) fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))

Tactic:
F.hasBiproduct_of_preserves _

Premises used: CategoryTheory.Functor.hasBiproduct_of_preserves
-- 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 M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.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)))
        (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)))
          (F.map
            (biproduct.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
          (biproduct.lift
            (Bicone.π
              (F.mapBicone
                (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
                  Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))))))
        (biproduct.π (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i) :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (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.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
          (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.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)))
      (Iso.hom (additiveObjIsoBiproduct F M) :
        F.obj M ⟶
          biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.π (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) 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) (M.X i))) =
    F.map
      (CategoryStruct.comp.{v₁, max 1 u₁} (Iso.hom.{v₁, max 1 u₁} M.isoBiproductEmbedding)
        (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))

Tactic:
dsimp [additiveObjIsoBiproduct]

Premises used: CategoryTheory.Mat_.additiveObjIsoBiproduct
-- 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.ι
rw :
  Eq (α := F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X 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)))
      (F.map (biproduct.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
      (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.lift
          (Bicone.π
            (F.mapBicone
              (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
                Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))))
        (biproduct.π (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i)))
    (F.map fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
⊢ Eq (α := F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.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)))
        (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)))
          (F.map
            (biproduct.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
          (biproduct.lift
            (Bicone.π
              (F.mapBicone
                (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
                  Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))))))
        (biproduct.π (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i) :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (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.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
          (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))

Tactic:
rw [biproduct.lift_π, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.lift_π
-- 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.ι
erw :
  Eq (α := F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (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.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
          (Bicone.π.{0, v₁, max 1 u₁}
            (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
              Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      F.obj M ⟶ F.obj ((fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))
    (F.map fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
⊢ Eq (α := F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X 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)))
      (F.map (biproduct.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
      (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.lift
          (Bicone.π
            (F.mapBicone
              (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
                Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))))
        (biproduct.π (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) i)))
    (F.map fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)

Tactic:
erw [biproduct.lift_π, ← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biproduct.lift_π
-- 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 M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (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.lift.{0, v₁, max 1 u₁} fun (i j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
          (Bicone.π.{0, v₁, max 1 u₁}
            (biproduct.bicone.{0, v₁, max 1 u₁} fun (i : M.ι) ↦
              Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      F.obj M ⟶ F.obj ((fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))
    (F.map fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
      F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))

Tactic:
simp