awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M : Mat_ C
i j : M.ι
⊢ 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)))
have 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 sorry 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 sorry else 0)
  (if h : j = i then eqToHom.{v₁, max 1 u₁} sorry else 0)
Tactic: simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc,
      biproduct.ι_π]
-- 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
M : Mat_ C
i j : M.ι
⊢ 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)
have 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 sorry 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 sorry else 0)
    PUnit.unit PUnit.unit)
  ((if h : j = i then eqToHom.{v₁, max 1 u₁} sorry else 0) PUnit.unit PUnit.unit)
Tactic: ext ⟨⟩ ⟨⟩
-- 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
M : Mat_ C
i j : M.ι
⊢ 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)
have w : Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (if h : j = i then eqToHom sorry else 0)
  ((if h : j = i then eqToHom.{v₁, max 1 u₁} sorry 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]
-- 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
M : Mat_ C
i j : M.ι
⊢ 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)
have pos : ∀ (h : j = i), Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (eqToHom sorry) (eqToHom.{v₁, max 1 u₁} sorry PUnit.unit PUnit.unit)
Tactic: split_ifs with h
-- 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
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)
⊢ 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)
have neg : ∀ (h : ¬j = i), Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) 0 (0 PUnit.unit PUnit.unit)
Tactic: split_ifs with h
-- 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
M : Mat_ C
i j : M.ι
h : j = i
⊢ Eq.{v₁ + 1} (α := M.X j ⟶ M.X i) (eqToHom ⋯) (eqToHom.{v₁, max 1 u₁} ⋯ PUnit.unit PUnit.unit)
have pos : Eq.{v₁ + 1} (α := M.X j ⟶ M.X j) (eqToHom sorry) (eqToHom.{v₁, max 1 u₁} sorry PUnit.unit PUnit.unit)
Tactic: subst h
Cleared hypotheses: i, h
-- 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₁
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.ι
⊢ 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))
have 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 sorry 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 sorry 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: dsimp [additiveObjIsoBiproduct]
-- 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₁
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)))
    (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)))
have 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 sorry 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 sorry else 0)
Tactic: rw [biproduct.lift_π, Category.assoc]
-- 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₁
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)))
    (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)
have 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 sorry 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 sorry else 0 :
    F.obj M ⟶ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
Tactic: erw [biproduct.lift_π, ← F.map_comp]
-- 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₁
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.ι
⊢ 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))
have 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 sorry 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 sorry else 0)) :
    F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) ⟶ F.obj M)
Tactic: dsimp [additiveObjIsoBiproduct, Functor.mapBiproduct, Functor.mapBicone]
-- 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₁
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.ι
⊢ 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)))
have 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 sorry 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: ext j : 1
-- 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₁
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 (α :=
    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))))
have 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 sorry else 0)
      (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom sorry else 0)))
  (F.map (Functor.map (embedding C) (f j i)))
Tactic: simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
    biproduct.ι_desc, ← F.map_comp]
-- 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₁
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 (α :=
    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)))
have 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 sorry else 0)
    (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom sorry else 0))
  (Functor.map (embedding C) (f j i))
Tactic: congr 1