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
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
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))))
⊢ 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)))

Tactic:
ext j k
-- 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
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.ι
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)
⊢ 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:
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
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)) ⟶ F.obj (Y.X k))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
        (L.map (Functor.map (embedding C) (f j k)) ≫
          α.hom.app (Y.X k) ≫ biproduct.lift fun (x : PUnit.{1}) ↦ 𝟙 (F.obj (Y.X k)))
        (biproduct.π (fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) PUnit.unit) :
      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ F.obj (Y.X k))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
        (α.hom.app (X.X j) ≫
            CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
              (biproduct.lift fun (x : PUnit.{1}) ↦ 𝟙 (F.obj (X.X j)) :
                F.obj (X.X j) ⟶ biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
              (biproduct.matrix fun (i j_1 : PUnit.{1}) ↦ F.map (f j k) :
                Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
                  (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))) :
          L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶
            biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
        (biproduct.π (fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) PUnit.unit :
          (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) ⟶ F.obj (Y.X k)) :
      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ F.obj (Y.X k))

Tactic:
simpa using α.hom.naturality (f j k)

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type (u₁ + 1)
inst : LargeCategory C
inst_1 : Preadditive C
inst_2 : HasFiniteBiproducts C
⊢ Eq (α := Mat_ C ⥤ C) (Equivalence.functor (equivalenceSelfOfHasFiniteBiproducts C)) (lift (𝟭 C))

Tactic:
rfl

Premises used: CategoryTheory.Mat_.lift, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type (u₁ + 1)
inst : LargeCategory C
inst_1 : Preadditive C
inst_2 : HasFiniteBiproducts C
⊢ Eq (α := C ⥤ Mat_ C) (Equivalence.inverse (equivalenceSelfOfHasFiniteBiproducts C)) (embedding C)

Tactic:
rfl

Premises used: CategoryTheory.Mat_.embedding, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
R : Type u
inst_2 : Semiring R
W X Y Z : Mat R
f : Matrix W.obj X.obj R
g : Matrix X.obj Y.obj R
h : Matrix Y.obj Z.obj R
⊢ HMul.hMul (α := Matrix W.obj Y.obj R)
      (have this :=
        HMul.hMul (α := Matrix W.obj X.obj R)
          (have this := f;
          this)
          (have this := g;
          this);
      this)
      (have this := h;
      this) =
    HMul.hMul (α := Matrix W.obj X.obj R)
      (have this := f;
      this)
      (have this :=
        HMul.hMul (α := Matrix X.obj Y.obj R)
          (have this := g;
          this)
          (have this := h;
          this);
      this)

Tactic:
simp [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
X Y : Mat R
f g : X ⟶ Y
h : ∀ (i : X.obj) (j : Y.obj), f i j = g i j
⊢ f = g

Tactic:
Matrix.ext_iff.mp h

Premises used: Iff.mp, Matrix.ext_iff
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M : Mat R
⊢ Eq (α := M ⟶ M) (𝟙 M) fun (i j : M.obj) ↦ if i = j then 1 else 0

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M : Mat R
i j : M.obj
⊢ Eq (α := R) (𝟙 M i j : R) (if i = j then 1 else 0 : R)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M : Mat R
i : M.obj
⊢ Eq (α := R) (𝟙 M i i : R) (1 : R)

Tactic:
simp [id_apply]

Premises used: CategoryTheory.Mat.id_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M : Mat R
i j : M.obj
h : i ≠ j
⊢ Eq (α := R) (𝟙 M i j : R) (0 : R)

Tactic:
simp [id_apply, h]

Premises used: CategoryTheory.Mat.id_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M N K : Mat R
f : M ⟶ N
g : N ⟶ K
⊢ f ≫ g = fun (i : M.obj) (k : K.obj) ↦ ∑ j : N.obj, f i j * g j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type u
inst : Semiring R
M N K : Mat R
f : M ⟶ N
g : N ⟶ K
i : M.obj
k : K.obj
⊢ (f ≫ g) i k = ∑ j : N.obj, f i j * g j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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ᵐᵒᵖ)
h : ∀ (i j : (FintypeCat.of X.ι).obj), Eq (α := R) (MulOpposite.unop (𝟙 X i j) : R) (𝟙 (FintypeCat.of X.ι) i j : 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.ι)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
h : Eq (α := R) (MulOpposite.unop (if h : i = j then eqToHom ⋯ else 0)) (if i = j then 1 else 0)
⊢ Eq (α := R) (MulOpposite.unop (𝟙 X i j) : R) (𝟙 (FintypeCat.of X.ι) i j : R)

Tactic:
simp only [Mat_.id_def, id_def]

Premises used: CategoryTheory.Mat_.id_def, CategoryTheory.Mat.id_def
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
neg : ¬i = j → Eq (α := R) (MulOpposite.unop 0) 0
⊢ Eq (α := R) (MulOpposite.unop (if h : i = j then eqToHom ⋯ else 0)) (if i = j then 1 else 0)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
h : i = j
⊢ Eq (α := R) (MulOpposite.unop (eqToHom ⋯)) 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
h : ¬i = j
⊢ Eq (α := R) (MulOpposite.unop 0) 0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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))
⊢ 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:
simp only [Mat_.comp_apply, comp_apply]

Premises used: CategoryTheory.Mat.comp_apply, CategoryTheory.Mat_.comp_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
⊢ Eq (α := R) (MulOpposite.unop (∑ x : Y.ι, f i x ≫ g x j)) (∑ x : Y.ι, MulOpposite.unop (f i x ≫ g x j))

Tactic:
Finset.unop_sum _ _

Premises used: Finset.unop_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
⊢ 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:
convert! Finset.unop_sum _ _

Premises used: Finset.unop_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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₂)
H : ∀ (i : X.ι) (j : Y.ι), a₁ i j = a₂ i j
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
⊢ Function.Injective (α := Rᵐᵒᵖ) MulOpposite.unop

Tactic:
MulOpposite.unop_injective

Premises used: MulOpposite.unop_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
H : MulOpposite.unop (a₁ i j) = MulOpposite.unop (a₂ i j)
⊢ a₁ i j = a₂ i j

Tactic:
apply_fun MulOpposite.unop using MulOpposite.unop_injective

Premises used: MulOpposite.unop, MulOpposite.unop_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
⊢ MulOpposite.unop (a₁ i j) = MulOpposite.unop (a₂ i j)

Tactic:
congr_fun (congr_fun w _) _

Premises used: MulOpposite.unop, congr_fun
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
⊢ MulOpposite.unop (a₁ i j) = MulOpposite.unop (a₂ i j)

Tactic:
exact congr_fun (congr_fun w _) _

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
R : Type
inst_2 : Ring R
X : Mat R
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 }
⊢ Functor.obj (equivalenceSingleObjInverse R)
      { ι := X.obj, fintype := FintypeCat.fintype, X := fun (x : X.obj) ↦ PUnit.unit : Mat_ (SingleObj Rᵐᵒᵖ) } =
    X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
R : Type
inst_2 : Ring R
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:
congr
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
R : Type
inst : Ring R
M N : Mat R
f g : M ⟶ N
i : M.obj
j : N.obj
⊢ (f + g) i j = f i j + g i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
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
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 ⟶ 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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)

Tactic:
have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr := by
    intro f
    ext
    · simp
    · simp [Category.assoc]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
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
h₁ :
  Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f 0) biprod.snd)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inl) biprod.snd)
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f 0) biprod.snd)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inl) biprod.snd)

Tactic:
simp [biprod.lift_snd, Category.assoc, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)

Tactic:
have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl := by
    intro f
    ext
    · simp
    · simp [biprod.lift_snd, Category.assoc, comp_zero]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
hl : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
f : X ⟶ Y
⊢ leftAdd X Y 0 f = f

Tactic:
simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_desc, CategoryTheory.Category.comp_id, CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
hl : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
f : X ⟶ Y
⊢ leftAdd X Y f 0 = f

Tactic:
simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_desc, CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd