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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
        (CategoryStruct.comp (Y :=
          Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
            (CokernelCofork.ofπ (Z :=
              biproduct.{w, v, u} (J := { j : J // j ≠ i })
                (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
              (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
          (Cofork.π
            (CokernelCofork.ofπ (Z :=
              biproduct.{w, v, u} (J := { j : J // j ≠ i })
                (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
              (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
          ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π)) =
      ι f j ≫ s.π
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      (Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π) =
    s.π

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 : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
w : (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        (Cofork.π
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π)) =
    ι f j ≫ s.π

Tactic:
rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_map_assoc, CategoryTheory.Limits.CokernelCofork.π_ofπ, CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
w : (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
w₁ : ∀ (h : ¬i = j), (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π

Tactic:
rcases Classical.em (i = j) with (rfl | h)

Premises used: Classical.em, Eq, rfl
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
w : 0 ≫ ι f i ≫ s.π = ι f i ≫ s.π
w₁ : 0 = ι f i ≫ s.π
w₂ w₃ : Eq.{v + 1} (α := f i ⟶ s.pt) 0 0
⊢ (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π

Tactic:
rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]

Premises used: Iff.mpr, Classical.not_not, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Limits.zero_comp, if_neg, rfl
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
h : ¬i = j
w : 𝟙 (f j) ≫ ι f j ≫ s.π = ι f j ≫ s.π
w₁ w₂ : ι f j ≫ s.π = ι f j ≫ s.π
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π

Tactic:
rw [if_pos (Ne.symm h), Category.id_comp]

Premises used: Ne.symm, if_pos, CategoryTheory.Category.id_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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
m :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
      (CokernelCofork.ofπ (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ⟶
    s.pt
hm :
  Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ≫
      m =
    s.π
rw :
  m =
    𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)) ≫
      m
⊢ m = (fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π

Tactic:
rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.fromSubtype_toSubtype, CategoryTheory.Limits.CokernelCofork.π_ofπ
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
m :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
      (CokernelCofork.ofπ (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ⟶
    s.pt
hm :
  Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ≫
      m =
    s.π
⊢ m =
    𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)) ≫
      m

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
m :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
      (CokernelCofork.ofπ (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ⟶
    s.pt
hm :
  Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ≫
      m =
    s.π
⊢ m =
    𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)) ≫
      m

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
⊢ HasCokernel.{v, u} (Y := biproduct.{w, v, u} f) (biproduct.ι f i)

Tactic:
HasColimit.mk ⟨_, biproduct.isColimitToSubtype f i⟩

Premises used: CategoryTheory.Limits.biproduct.isColimitToSubtype, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.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, 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
-- 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
⊢ 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 k.2]

Premises used: dif_neg, 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ᶜ
⊢ 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
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
⊢ 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, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg k.2]
        simp only [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
-- 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
w₁ :
  ∀ (j : K),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
          ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
                (x_1 :
                  Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                    (g ≫ biproduct.toSubtype f p) 0) ↦
              (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
            g' w)
          (biproduct.fromSubtype f pᶜ))
        (biproduct.π f j) =
      g' ≫ biproduct.π f j
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
      ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
            (x_1 :
              Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                (g ≫ biproduct.toSubtype f p) 0) ↦
          (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
        g' w)
      (biproduct.fromSubtype f pᶜ) =
    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' : 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
w₁ : (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
              (x_1 :
                Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                  (g ≫ biproduct.toSubtype f p) 0) ↦
            (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
          g' w)
        (biproduct.fromSubtype f pᶜ))
      (biproduct.π f j) =
    g' ≫ biproduct.π f j

Tactic:
simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Limits.biproduct.toSubtype_fromSubtype, Pi.compl_apply