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
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 (α :=
    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))
have 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 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)
      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: funext ⟨⟩ ⟨⟩
-- 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
⊢ 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 N)
    (Iso.inv (additiveObjIsoBiproduct F M) ≫ F.map f :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj N)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
        (biproduct.matrix fun (i : M.ι) (j : N.ι) ↦ F.map (Functor.map (embedding C) (f i j)) :
          Quiver.Hom.{v₁, u₁} (V := D)
            (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₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j))))
        (Iso.inv (additiveObjIsoBiproduct F N) :
          (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
            F.obj N) :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj N)
have rw : F.map f =
  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)))
    (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
        (biproduct.matrix fun (i : M.ι) (j : N.ι) ↦ F.map (Functor.map (embedding C) (f i j)) :
          Quiver.Hom.{v₁, u₁} (V := D)
            (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₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j))))
        (Iso.inv (additiveObjIsoBiproduct F N) :
          (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
            F.obj N) :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj N)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]
-- 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₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
⊢ 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)))
have 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))
Tactic: ext 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
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.ι
⊢ 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))
have pos : ∀ (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: by_cases h : j = 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
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))
have 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))
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
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
L : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_6 : L.Additive
α : embedding C ⋙ L ≅ F
X Y : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} X Y
⊢ Eq.{v₁ + 1} (α :=
    (j : X.ι) →
      (k : Y.ι) → L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ (embedding C ⋙ lift F).obj (Y.X k))
    (fun (j : X.ι) (k : Y.ι) ↦
      L.map (Functor.map (embedding C) (f j k)) ≫
        Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)))
    fun (j : X.ι) (k : Y.ι) ↦
    Iso.hom (α.app (X.X j)) ≫
      CategoryStruct.comp (Y := (embedding C ⋙ lift F).obj (X.X j))
        (Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X j)))
        (Functor.map (lift F) (Functor.map (embedding C) (f j k)))
have e_a : ∀ (j : X.ι) (k : Y.ι),
  Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ (embedding C ⋙ lift F).obj (Y.X k))
    (L.map (Functor.map (embedding C) (f j k)) ≫
      Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)))
    (Iso.hom (α.app (X.X j)) ≫
      CategoryStruct.comp (Y := (embedding C ⋙ lift F).obj (X.X j))
        (Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X j)))
        (Functor.map (lift F) (Functor.map (embedding C) (f j k))))
Tactic: ext j k
-- 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₁, u₁, u₁} C D
inst_5 : F.Additive
L : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_6 : L.Additive
α : embedding C ⋙ L ≅ F
X Y : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} X Y
j : X.ι
k : Y.ι
⊢ Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ (embedding C ⋙ lift F).obj (Y.X k))
    (L.map (Functor.map (embedding C) (f j k)) ≫
      Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)))
    (Iso.hom (α.app (X.X j)) ≫
      CategoryStruct.comp (Y := (embedding C ⋙ lift F).obj (X.X j))
        (Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X j)))
        (Functor.map (lift F) (Functor.map (embedding C) (f j k))))
have e_a : ∀ (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι),
  CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
        F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
      (L.map (Functor.map (embedding C) (f j k)) ≫
          Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)) :
        L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ (embedding C ⋙ lift F).obj (Y.X k))
      (biproduct.π
        (fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
          F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
        j_1) =
    CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
        F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
      (Iso.hom (α.app (X.X j)) ≫
        CategoryStruct.comp (Y := (embedding C ⋙ lift F).obj (X.X j))
          (Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X j)))
          (Functor.map (lift F) (Functor.map (embedding C) (f j k))))
      (biproduct.π
        (fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
          F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
        j_1)
Tactic: apply biproduct.hom_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
R : Type
inst_2 : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
⊢ Eq (α := FintypeCat.of X.ι ⟶ FintypeCat.of X.ι)
    (fun (i j : (FintypeCat.of X.ι).obj) ↦ (MulOpposite.unop (𝟙 X i j) : R))
    (𝟙 (FintypeCat.of X.ι) : FintypeCat.of X.ι ⟶ FintypeCat.of X.ι)
have h : ∀ (i j : (FintypeCat.of X.ι).obj), Eq (α := R) (MulOpposite.unop (𝟙 X i j) : R) (𝟙 (FintypeCat.of X.ι) i j : R)
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
R : Type
inst_2 : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i j : (FintypeCat.of X.ι).obj
⊢ Eq (α := R) (MulOpposite.unop (𝟙 X i j) : R) (𝟙 (FintypeCat.of X.ι) i j : R)
have h : Eq (α := R) (MulOpposite.unop (if h : i = j then eqToHom sorry else 0)) (if i = j then 1 else 0)
Tactic: simp only [Mat_.id_def, 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
R : Type
inst_2 : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i j : (FintypeCat.of X.ι).obj
⊢ Eq (α := R) (MulOpposite.unop (if h : i = j then eqToHom ⋯ else 0)) (if i = j then 1 else 0)
have pos : ∀ (h : i = j), Eq (α := R) (MulOpposite.unop (eqToHom sorry)) 1
Tactic: split_ifs
-- 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
R : Type
inst_2 : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i j : (FintypeCat.of X.ι).obj
pos : ∀ (h : i = j), Eq (α := R) (MulOpposite.unop (eqToHom ⋯)) 1
⊢ Eq (α := R) (MulOpposite.unop (if h : i = j then eqToHom ⋯ else 0)) (if i = j then 1 else 0)
have neg : ¬i = j → Eq (α := R) (MulOpposite.unop 0) 0
Tactic: split_ifs
-- 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
R : Type
inst_2 : Ring R
X Y Z : Mat_ (SingleObj Rᵐᵒᵖ)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := FintypeCat.of X.ι ⟶ FintypeCat.of Z.ι)
    (fun (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Z.ι).obj) ↦ MulOpposite.unop ((f ≫ g) i j))
    (CategoryStruct.comp (Y := FintypeCat.of Y.ι)
      (fun (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Y.ι).obj) ↦ MulOpposite.unop (f i j))
      fun (i : (FintypeCat.of Y.ι).obj) (j : (FintypeCat.of Z.ι).obj) ↦ MulOpposite.unop (g i j))
have h : ∀ (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Z.ι).obj),
  MulOpposite.unop ((f ≫ g) i j) =
    CategoryStruct.comp (Y := FintypeCat.of Y.ι)
      (fun (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Y.ι).obj) ↦ MulOpposite.unop (f i j))
      (fun (i : (FintypeCat.of Y.ι).obj) (j : (FintypeCat.of Z.ι).obj) ↦ MulOpposite.unop (g i j)) i 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
R : Type
inst_2 : Ring R
X Y Z : Mat_ (SingleObj Rᵐᵒᵖ)
f : X ⟶ Y
g : Y ⟶ Z
i : (FintypeCat.of X.ι).obj
j : (FintypeCat.of Z.ι).obj
⊢ MulOpposite.unop ((f ≫ g) i j) =
    CategoryStruct.comp (Y := FintypeCat.of Y.ι)
      (fun (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Y.ι).obj) ↦ MulOpposite.unop (f i j))
      (fun (i : (FintypeCat.of Y.ι).obj) (j : (FintypeCat.of Z.ι).obj) ↦ MulOpposite.unop (g i j)) i j
have h : Eq (α := R) (MulOpposite.unop (∑ j_1 : Y.ι, f i j_1 ≫ g j_1 j))
  (∑ j_1 : Y.ι, MulOpposite.unop (f i j_1) * MulOpposite.unop (g j_1 j))
Tactic: simp only [Mat_.comp_apply, comp_apply]
-- 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
R : Type
inst_2 : Ring R
X Y : Mat_ (SingleObj Rᵐᵒᵖ)
a₁ a₂ : X ⟶ Y
w :
  Eq (α := Functor.obj (equivalenceSingleObjInverse R) X ⟶ Functor.obj (equivalenceSingleObjInverse R) Y)
    (Functor.map (equivalenceSingleObjInverse R) a₁) (Functor.map (equivalenceSingleObjInverse R) a₂)
⊢ a₁ = a₂
have H : ∀ (i : X.ι) (j : Y.ι), a₁ i j = a₂ i 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
R : Type
inst_2 : Ring R
X Y : Mat_ (SingleObj Rᵐᵒᵖ)
a₁ a₂ : X ⟶ Y
w :
  Eq (α := Functor.obj (equivalenceSingleObjInverse R) X ⟶ Functor.obj (equivalenceSingleObjInverse R) Y)
    (Functor.map (equivalenceSingleObjInverse R) a₁) (Functor.map (equivalenceSingleObjInverse R) a₂)
i : X.ι
j : Y.ι
⊢ a₁ i j = a₂ i j
have H : MulOpposite.unop (a₁ i j) = MulOpposite.unop (a₂ i j)
Tactic: apply_fun MulOpposite.unop using MulOpposite.unop_injective
-- 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
R : Type
inst_2 : Ring R
X : Mat R
⊢ Functor.obj (equivalenceSingleObjInverse R)
      { ι := X.obj, fintype := FintypeCat.fintype, X := fun (x : X.obj) ↦ PUnit.unit : Mat_ (SingleObj Rᵐᵒᵖ) } =
    X
have mk : ∀ (obj : Type) (property : Finite obj),
  Functor.obj (equivalenceSingleObjInverse R)
      {
        ι :=
          ObjectProperty.FullSubcategory.obj
            { obj := obj, property := property : ObjectProperty.FullSubcategory Finite },
        fintype := FintypeCat.fintype,
        X :=
          fun
            (x :
              ObjectProperty.FullSubcategory.obj
                { obj := obj, property := property : ObjectProperty.FullSubcategory Finite }) ↦
          PUnit.unit :
        Mat_ (SingleObj Rᵐᵒᵖ) } =
    { obj := obj, property := property }
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
have h₀ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift 0 f) biprod.fst)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inr) biprod.fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f : X ⟶ Y
h₀ :
  Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift 0 f) biprod.fst)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inr) biprod.fst)
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift 0 f) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inr) biprod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ leftAdd X Y x1 x2) 0
have hr : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
Tactic: have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr := by
    intro f
    ext
    · simp
    · simp [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
hr : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
f : X ⟶ Y
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f 0) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inl) biprod.fst
Tactic: ext