awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j : f j ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
          (π g k : biproduct.{0, v, u} g ⟶ g k) :
        biproduct.{0, v, u} f ⟶ g k) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc fun (j : J) ↦ m j k)

Tactic:
simp [biproduct.matrix]

Premises used: CategoryTheory.Limits.biproduct.matrix
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
⊢ Eq (α := f j ⟶ biproduct.{0, v, u} g)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j : f j ⟶ biproduct.{0, v, u} f)
        (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
      f j ⟶ biproduct.{0, v, u} g)
    (lift fun (k : K) ↦ m j k : f j ⟶ biproduct.{0, v, u} g)

Tactic:
simp [biproduct.matrix]

Premises used: CategoryTheory.Limits.biproduct.matrix
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
k : K
⊢ components (matrix m) j k = m j k

Tactic:
simp [biproduct.components]

Premises used: CategoryTheory.Limits.biproduct.components
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g
w :
  ∀ (j : K) (j_1 : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g)
            (matrix fun (j : J) (k : K) ↦ components m j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
            (π g j : biproduct.{0, v, u} g ⟶ g j) :
          biproduct.{0, v, u} f ⟶ g j) =
      ι f j_1 ≫ m ≫ π g j
⊢ (matrix fun (j : J) (k : K) ↦ components m j k) = m

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g
j : K
j_1 : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g)
          (matrix fun (j : J) (k : K) ↦ components m j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
          (π g j : biproduct.{0, v, u} g ⟶ g j) :
        biproduct.{0, v, u} f ⟶ g j) =
    ι f j_1 ≫ m ≫ π g j

Tactic:
simp [biproduct.components]

Premises used: CategoryTheory.Limits.biproduct.components
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J_2 : Type w
K_1 : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type
inst_6 : Finite J
K : Type
inst_7 : Finite K
C : Type u
inst_8 : Category.{v, u} C
inst_9 : HasZeroMorphisms.{v, u} C
inst_10 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
h : ∀ (x : J) (x_1 : K), components (matrix m) x x_1 = m x x_1
⊢ components (matrix m) = m

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J_2 : Type w
K_1 : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type
inst_6 : Finite J
K : Type
inst_7 : Finite K
C : Type u
inst_8 : Category.{v, u} C
inst_9 : HasZeroMorphisms.{v, u} C
inst_10 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
x : J
x_1 : K
⊢ components (matrix m) x x_1 = m x x_1

Tactic:
apply biproduct.matrix_components

Premises used: CategoryTheory.Limits.biproduct.matrix_components
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : J
⊢ IsSplitMono.{v, u} (Y := biproduct.{w, v, u} f) (ι f b)

Tactic:
(biproduct.bicone f).instIsSplitMonoι b

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.instIsSplitMonoι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : J
⊢ IsSplitEpi.{v, u} (X := biproduct.{w, v, u} f) (π f b)

Tactic:
(biproduct.bicone f).instIsSplitEpiπ b

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.instIsSplitEpiπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ Eq (α := b.toCone.pt ⟶ Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)))
    (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (lift b.π)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Discrete.natTrans, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ Eq (α := Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι)

Tactic:
biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.Bicone.IsBilimit.isLimit, CategoryTheory.Limits.biproduct.hom_ext'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
refine :
  ∀ (j : J) (j' : Discrete J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
        b.toCone.π.app j' =
      CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ Eq (α := Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι)

Tactic:
refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.Bicone.IsBilimit.isLimit, CategoryTheory.Limits.biproduct.hom_ext'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₃ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₄ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) = b.ι j ≫ b.toCone.π.app j'
rw₅ : (if h : j = j'.as then eqToHom ⋯ else 0) = b.ι j ≫ b.toCone.π.app j'
rw₆ :
  Eq (α := f j ⟶ obj.{w, v, w, u} (Discrete.functor f) j') (if h : j = j'.as then eqToHom ⋯ else 0) (b.ι j ≫ b.π j'.as)
rw₇ rw₈ :
  Eq.{v + 1} (α := f j ⟶ obj.{w, v, w, u} (Discrete.functor f) j') (if h : j = j'.as then eqToHom ⋯ else 0)
    (if h : j = j'.as then eqToHom ⋯ else 0)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'

Tactic:
rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.Limits.biproduct.bicone_π, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.Bicone.toCone_π_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
refine :
  ∀ (j : J) (j' : Discrete J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
        b.toCone.π.app j' =
      CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ Eq (α := Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι)

Tactic:
classical
  refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
  rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.Limits.biproduct.bicone_π, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.Bicone.toCone_π_app, CategoryTheory.Limits.Bicone.IsBilimit.isLimit, CategoryTheory.Limits.biproduct.hom_ext'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
      (desc b.ι) =
    𝟙 b.pt
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) =
    𝟙 b.pt
rw₂ rw₃ : Eq.{v + 1} (α := b.pt ⟶ b.pt) (𝟙 b.pt) (𝟙 b.pt)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift b.π) (desc b.ι) = 𝟙 b.pt

Tactic:
rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw : desc b.ι ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) = 𝟙 (biproduct.{w, v, u} f)
rw₁ :
  Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) =
    𝟙 (biproduct.{w, v, u} f)
rw₂ rw₃ :
  Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} f) (𝟙 (biproduct.{w, v, u} f))
    (𝟙 (biproduct.{w, v, u} f))
⊢ desc b.ι ≫ lift b.π = 𝟙 (biproduct.{w, v, u} f)

Tactic:
rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv, CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
⊢ HasZeroObject.{v, u} C

Tactic:
⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩

Premises used: Unique.mk, Empty.elim, CategoryTheory.Limits.HasZeroObject.mk, Nonempty.intro, Exists.intro, CategoryTheory.Limits.biproduct, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
refine_1 : ∀ (X : C) (a : biproduct.{0, v, u} Empty.elim ⟶ X), a = default
refine_2 : ∀ (X : C) (a : X ⟶ biproduct.{0, v, u} Empty.elim), a = default
⊢ HasZeroObject.{v, u} C

Tactic:
refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : biproduct.{0, v, u} Empty.elim ⟶ X
refine_1 :
  ∀ (j : Empty),
    biproduct.ι Empty.elim j ≫ a =
      CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) (biproduct.ι Empty.elim j) default
⊢ a = default

Tactic:
apply biproduct.hom_ext'

Premises used: CategoryTheory.Limits.biproduct.hom_ext'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : biproduct.{0, v, u} Empty.elim ⟶ X
⊢ ∀ (j : Empty),
    biproduct.ι Empty.elim j ≫ a =
      CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) (biproduct.ι Empty.elim j) default

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : X ⟶ biproduct.{0, v, u} Empty.elim
refine_2 :
  ∀ (j : Empty),
    a ≫ biproduct.π Empty.elim j =
      CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) default (biproduct.π Empty.elim j)
⊢ a = default

Tactic:
apply biproduct.hom_ext

Premises used: CategoryTheory.Limits.biproduct.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : X ⟶ biproduct.{0, v, u} Empty.elim
⊢ ∀ (j : Empty),
    a ≫ biproduct.π Empty.elim j =
      CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) default (biproduct.π Empty.elim j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
e_a : default = j
⊢ f default = f j

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
e_a : j = j
e_a₁ : J
e_a₂ : j = j
e_a₃ : J
⊢ default = j

Tactic:
rw [← Unique.uniq]

Premises used: Unique.uniq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
e_a : j = default
⊢ f j = f default

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
e_a : j = j
e_a₁ : J
e_a₂ : j = j
e_a₃ : J
⊢ j = default

Tactic:
rw [← Unique.uniq]

Premises used: Unique.uniq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Subsingleton J
inst_11 : Nonempty J
f : J → C
⊢ HasBiproduct.{w, v, u} f

Tactic:
let ⟨_⟩ := nonempty_unique J; .mk (limitBiconeOfUnique f)

Premises used: CategoryTheory.Limits.HasBiproduct, _private.0.CategoryTheory.Limits.hasBiproduct_unique.match_1, CategoryTheory.Limits.limitBiconeOfUnique, CategoryTheory.Limits.HasBiproduct.mk, nonempty_unique
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
i : WalkingPair
left : s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt
right : s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt
⊢ s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
⊢ s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt

Tactic:
exact Fan.IsLimit.lift h₁ (fun a ↦ s.proj (.inl a))

Premises used: CategoryTheory.Limits.Fan.proj, Sum.inl, CategoryTheory.Limits.Fan.IsLimit.lift