awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ biproduct.{0, v, u} f
w : Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0
j : K
pos : ∀ (h : (p j)ᶜ), g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f j
neg : ∀ (h : ¬(p j)ᶜ), g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j
⊢ (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j

Tactic:
split_ifs with h
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ biproduct.{0, v, u} f
w : Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0
j : K
h : (p j)ᶜ
⊢ g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f 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 : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ biproduct.{0, v, u} f
w : Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0
j : K
h : ¬(p j)ᶜ
⊢ Eq (α := W' ⟶ Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j ⋯))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (g' ≫ biproduct.toSubtype f p)
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) 0
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)))

Tactic:
replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ biproduct.{0, v, u} f
j : K
h : ¬(p j)ᶜ
w :
  Eq (α := W' ⟶ Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j ⋯))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (g' ≫ biproduct.toSubtype f p)
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) 0
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)))
⊢ g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j

Tactic:
simpa using w.symm

Premises used: Eq.symm
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
⊢ HasKernel.{v, u} (X := biproduct.{0, v, u} f) (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
    (biproduct.toSubtype f p)

Tactic:
HasLimit.mk (kernelForkBiproductToSubtype f p)

Premises used: CategoryTheory.Limits.kernelForkBiproductToSubtype, CategoryTheory.Limits.HasLimit.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 : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
w :
  ∀ (j : Subtype pᶜ) (k : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
        (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.fromSubtype f p) (biproduct.toSubtype f pᶜ))
          (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
        (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
          (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))
⊢ Eq.{v + 1} (α :=
    biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶
      biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.fromSubtype f p) (biproduct.toSubtype f pᶜ)) 0

Tactic:
ext j k
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
w :
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
      (if h : (p (↑k : K))ᶜ then
        biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) (Subtype.mk (p := pᶜ) (↑k : K) h)
      else 0)
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
    0
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.fromSubtype f p) (biproduct.toSubtype f pᶜ))
        (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
        (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))

Tactic:
simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.biproduct.ι_toSubtype_assoc, Pi.compl_apply
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
w :
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
    0
w₁ : ¬(p (↑k : K))ᶜ
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
      (if h : (p (↑k : K))ᶜ then
        biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) (Subtype.mk (p := pᶜ) (↑k : K) h)
      else 0)
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
    0

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
      (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
    0

Tactic:
simp only [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p (↑k : K))ᶜ

Tactic:
not_not.mpr k.2

Premises used: Iff.mpr, Classical.not_not, Subtype.property
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p (↑k : K))ᶜ

Tactic:
exact not_not.mpr k.2

Premises used: Iff.mpr, Classical.not_not, Subtype.property
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
w :
  ∀ (j : Subtype pᶜ) (k : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
        (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.fromSubtype f p) (biproduct.toSubtype f pᶜ))
          (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
        (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) k)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
          (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j)))
w₁ :
  ∀ (j : Subtype pᶜ) (k : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (if h : (p (↑k : K))ᶜ then
          biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) (Subtype.mk (p := pᶜ) (↑k : K) h)
        else 0)
        (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
      0
w₂ :
  ∀ (j : Subtype pᶜ) (k : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : K) ↦ C) p f k ⟶ Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)) 0
        (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) j))
      0
w₃ w₄ : ∀ (j : Subtype pᶜ) (k : Subtype p), ¬(p (↑k : K))ᶜ
⊢ Eq.{v + 1} (α :=
    biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶
      biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.fromSubtype f p) (biproduct.toSubtype f pᶜ)) 0

Tactic:
classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, dif_neg, CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.biproduct.ι_toSubtype_assoc, Pi.compl_apply
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
w₁ :
  ∀ (j : K),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          (biproduct.toSubtype f pᶜ)
          ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
                (x_1 :
                  Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                    (biproduct.fromSubtype f p ≫ g) 0) ↦
              (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
            g' w)) =
      biproduct.ι f j ≫ g'
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
      (biproduct.toSubtype f pᶜ)
      ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
            (x_1 :
              Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                (biproduct.fromSubtype f p ≫ g) 0) ↦
          (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
        g' w) =
    g'

Tactic:
ext j
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
w₁ : (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w)) =
    biproduct.ι f j ≫ g'

Tactic:
simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_map_assoc, CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
pos : ∀ (h : (p j)ᶜ), 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
neg : ∀ (h : ¬(p j)ᶜ), 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
⊢ (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
split_ifs with h
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
h : (p j)ᶜ
⊢ 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

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 : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
h : ¬(p j)ᶜ
⊢ Eq (α := Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j ⋯) ⟶ W)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯))
      (biproduct.fromSubtype f p ≫ g'))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)) 0)

Tactic:
replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
j : K
h : ¬(p j)ᶜ
w :
  Eq (α := Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j ⋯) ⟶ W)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯))
      (biproduct.fromSubtype f p ≫ g'))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
      (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j ⋯)) 0)
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
simpa using w.symm

Premises used: Eq.symm
-- 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 : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
⊢ HasCokernel.{v, u} (X := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (Y :=
    biproduct.{0, v, u} f) (biproduct.fromSubtype f p)

Tactic:
HasColimit.mk (cokernelCoforkBiproductFromSubtype f p)

Premises used: CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype, CategoryTheory.Limits.HasColimit.mk
-- 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
w :
  ∀ (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)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ g k)
    (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)
    (desc fun (j : J) ↦ m j k : biproduct.{0, v, u} f ⟶ g k)

Tactic:
ext