awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) 0
pos₁ :
  ∀ (j_1 : Subtype p) (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 (eqToHom ⋯)
neg₁ :
  ∀ (j_1 : Subtype p) (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 0
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)

Tactic:
classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.toSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.lift_π, 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j ⟶ biproduct.{w, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) (fromSubtype f p))
    (ι f (↑j : J))

Tactic:
biproduct.ι_desc _ _

Premises used: CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Limits.biproduct.fromSubtype
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))

Tactic:
biproduct.hom_ext _ _ fun j => ?_

Premises used: 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
refine :
  ∀ (j : Subtype p),
    CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
      𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
        π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))

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

Premises used: 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₂ :
  π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₃ rw₄ :
  Eq.{v + 1} (α :=
    biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j)
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j

Tactic:
rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.fromSubtype_π_subtype, CategoryTheory.Limits.biproduct.toSubtype_π, CategoryTheory.Category.id_comp
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
w :
  ∀ (i : J),
    Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
          (fromSubtype f p))
        (π f i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
      (fromSubtype f p))
    (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0)

Tactic:
ext1 i
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
i : J
pos :
  ∀ (h : p i),
    Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
          (fromSubtype f p))
        (π f i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
neg :
  ∀ (h : ¬p i),
    Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
          (fromSubtype f p))
        (π f i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))

Tactic:
by_cases h : p i
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
i : J
h : p i
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))

Tactic:
simp [h]
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
i : J
h : ¬p i
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))

Tactic:
simp [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 : 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)
⊢ Eq.{v + 1} (α :=
    biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f) ⟶
      f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f fun (j : J) ↦ j ≠ i) (π f i)) 0

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 : 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (CategoryStruct.comp (Y :=
          Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
            (KernelFork.ofι (Z :=
              biproduct.{w, v, u} (J := { j : J // j ≠ i })
                (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
              (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯))
          (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
          (Fork.ι
            (KernelFork.ofι (Z :=
              biproduct.{w, v, u} (J := { j : J // j ≠ i })
                (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
              (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)))
        (π f j) =
      s.ι ≫ π f j
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
      (Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)) =
    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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
j : J
w : (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y :=
        Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
        (Fork.ι
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)))
      (π f j) =
    s.ι ≫ π f j

Tactic:
rw [KernelFork.ι_ofι, Category.assoc, Category.assoc,
        biproduct.toSubtype_fromSubtype_assoc, biproduct.map_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.KernelFork.ι_ofι, CategoryTheory.Limits.biproduct.map_π, 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
w : s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i
w₁ : s.ι ≫ 0 = s.ι ≫ π f i
w₂ : 0 = s.ι ≫ π f i
w₃ w₄ : Eq.{v + 1} (α := s.pt ⟶ f i) 0 0
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i

Tactic:
rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]

Premises used: Iff.mpr, Classical.not_not, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.KernelFork.condition, 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
j : J
h : ¬i = j
w : s.ι ≫ π f j ≫ 𝟙 (f j) = s.ι ≫ π f j
w₁ w₂ : s.ι ≫ π f j = s.ι ≫ π f j
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j

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

Premises used: Ne.symm, CategoryTheory.Category.comp_id, if_pos
-- 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
m :
  s.pt ⟶
    Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
      (KernelFork.ofι (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)
hm :
  m ≫
      Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯) =
    s.ι
rw :
  m =
    m ≫
      𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
⊢ m = s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i

Tactic:
rw [← hm, KernelFork.ι_ofι, Category.assoc, biproduct.fromSubtype_toSubtype]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.KernelFork.ι_ofι, CategoryTheory.Limits.biproduct.fromSubtype_toSubtype
-- 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
m :
  s.pt ⟶
    Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
      (KernelFork.ofι (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)
hm :
  m ≫
      Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯) =
    s.ι
⊢ m =
    m ≫
      𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, 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 : 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 : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
m :
  s.pt ⟶
    Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
      (KernelFork.ofι (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)
hm :
  m ≫
      Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯) =
    s.ι
⊢ m =
    m ≫
      𝟙
        (biproduct.{w, v, u} (J := { j : J // j ≠ i })
          (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, 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 : 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)
⊢ HasKernel.{v, u} (X := biproduct.{w, v, u} f) (biproduct.π f i)

Tactic:
HasLimit.mk ⟨_, biproduct.isLimitFromSubtype f i⟩

Premises used: CategoryTheory.Limits.biproduct.isLimitFromSubtype, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.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 : 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)
⊢ Eq.{v + 1} (α :=
    f i ⟶
      biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f i) (toSubtype f fun (j : J) ↦ j ≠ i)) 0

Tactic:
simp