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
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)
have neg : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') 0 (if h : j = j' then eqToHom sorry else 0)
Tactic: rw [dif_neg h, dif_neg (Ne.symm 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
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
neg : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') 0 (if h : j = j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)
have neg₁ : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') 0 0
Tactic: rw [dif_neg h, dif_neg (Ne.symm 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
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (if h : i' = i then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
have neg : ¬(i = i' ∧ j ≍ j')
Tactic: rw [dif_neg h, dif_neg]
-- 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
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
⊢ ¬(i = i' ∧ j ≍ j')
have neg : i = i' → j ≍ j' → False
Tactic: tauto
-- 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_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
M : Mat_ C
⊢ Eq.{(max 1 u₁) + 1} (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)
have mk : ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C),
  Eq.{(max 1 u₁) + 1} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C })
    (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C))
      { ι := ι, fintype := fintype, X := X : Mat_ C })
Tactic: cases M
Cleared hypotheses: M
-- 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_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 : Mat_ C
⊢ Eq.{(max 1 u_2) + 1} (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)
have mk : ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C),
  Eq.{(max 1 u_2) + 1}
    (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C })
    (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_)
      { ι := ι, fintype := fintype, X := X : Mat_ C })
Tactic: cases M
Cleared hypotheses: M
-- 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
x : C
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x })
    (fun (x_1 x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_2 : PUnit.{1}) ↦ x }) ↦ 𝟙 x)
    (CategoryStruct.id.{v₁, max 1 u₁} { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x })
have H : ∀ (j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }),
  Eq.{v₁ + 1} (α :=
    (fun (i j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }) ↦
        Quiver.Hom.{v₁, u₁} (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x : Mat_ C } i)
          (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x } j))
      PUnit.unit j)
    (𝟙 x)
    (CategoryStruct.id.{v₁, max 1 u₁} { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
      PUnit.unit j)
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
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X }
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z })
    (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
        (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
      x ≫ x_1)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
      (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
          (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y }) ↦
        x)
      fun (x : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
        (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
      x_1)
have H : ∀ (j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }),
  x ≫ x_1 =
    CategoryStruct.comp.{v₁, max 1 u₁} (Y := { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
      (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
          (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y }) ↦
        x)
      (fun (x : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
          (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
        x_1)
      PUnit.unit j
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
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
    (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 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
        if h : j = i then eqToHom ⋯ else 0)
      (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))
    (CategoryStruct.id.{v₁, max 1 u₁} M)
have simp : Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
  (∑ j : M.ι,
    CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
      (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
        if h : j_1 = j then eqToHom sorry else 0)
      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.id.{v₁, max 1 u₁} M)
Tactic: simp only [biproduct.lift_desc]
-- 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
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
    (∑ j : M.ι,
      CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
          if h : j_1 = j then eqToHom ⋯ else 0)
        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.id.{v₁, max 1 u₁} M)
have h : ∀ (i j : M.ι),
  Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    ((∑ j : M.ι,
          CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
            (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
              if h : j_1 = j then eqToHom sorry else 0)
            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)
        i j :
      (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    (CategoryStruct.id.{v₁, max 1 u₁} M i j : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
Tactic: funext i j
-- 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 j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    ((∑ j : M.ι,
          CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
            (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
              if h : j_1 = j then eqToHom ⋯ else 0)
            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)
        i j :
      (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    (CategoryStruct.id.{v₁, max 1 u₁} M i j : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
have h : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
  ((∑ j : M.ι,
      CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom sorry else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
        if h : j = k then eqToHom sorry else 0)
    i j)
  (if h : i = j then eqToHom sorry else 0)
Tactic: dsimp [id_def]
-- 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 i ⟶ M.X j)
    ((∑ j : M.ι,
        CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
          (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom ⋯ else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
      i j)
    (if h : i = j then eqToHom ⋯ else 0)
have h : 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 sorry else 0)
    (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom sorry else 0) i j)
  (if h : i = j then eqToHom sorry else 0)
Tactic: rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]
-- 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 :
  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)
⊢ Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    ((∑ j : M.ι,
        CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
          (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom ⋯ else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
      i j)
    (if h : i = j then eqToHom ⋯ else 0)
have h₁ : ∀ (b : M.ι),
  Membership.mem (γ := Finset M.ι) Finset.univ b →
    b ≠ i →
      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 sorry else 0)
          (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : b = k then eqToHom sorry else 0) i j)
        0
Tactic: rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]
-- 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 :
  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)
h₁ :
  ∀ (b : M.ι),
    Membership.mem (γ := Finset M.ι) Finset.univ b →
      b ≠ i →
        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
⊢ Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    ((∑ j : M.ι,
        CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
          (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom ⋯ else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
      i j)
    (if h : i = j then eqToHom ⋯ else 0)
have 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 sorry else 0)
      (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom sorry else 0) i j)
    0
Tactic: rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]
-- 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 b : M.ι
h : Membership.mem (γ := Finset M.ι) Finset.univ b
hb : b ≠ i
⊢ 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
have 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 sorry else 0) (if h : b = j then eqToHom sorry else 0))
  0
Tactic: dsimp
-- 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 b : M.ι
h : Membership.mem (γ := Finset M.ι) Finset.univ b
hb : b ≠ i
⊢ 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
have 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 sorry else 0) (if h : b = j then eqToHom sorry else 0))
  0
Tactic: rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_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
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
⊢ 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
have h₁ : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
  (CategoryStruct.comp (Y := M.X b) (if h : i = b then eqToHom sorry else 0) (if h : b = j then eqToHom sorry else 0)) 0
Tactic: rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_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
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
⊢ 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
have h₂ : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j) (CategoryStruct.comp (Y := M.X b) 0 (if h : b = j then eqToHom sorry else 0)) 0
Tactic: rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_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
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
⊢ 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
have h₃ : Eq.{v₁ + 1} (α := M.X i ⟶ M.X j) 0 0
Tactic: rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_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
M : Mat_ C
⊢ 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)))
have 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 sorry 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 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)) 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))
Tactic: apply biproduct.hom_ext