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

Tactic:
classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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.Limits.biproduct.fromSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.ι_desc_assoc, 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} (α := biproduct.{w, v, u} f ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j)
    (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))
    (π f (↑j : J))

Tactic:
biproduct.lift_π _ _

Premises used: CategoryTheory.Limits.biproduct.toSubtype, CategoryTheory.Limits.biproduct.lift_π
-- 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
j : J
w :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
      (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) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
    (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)

Tactic:
ext 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
j : J
i : Subtype p
w :
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
    (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) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))

Tactic:
rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.toSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.lift_π
-- 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
j : J
i : Subtype p
pos :
  ∀ (h : p j),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
neg :
  ∀ (h : ¬p j),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))

Tactic:
by_cases h : p j
-- 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
j : J
i : Subtype p
h : p j
pos :
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))

Tactic:
rw [dif_pos h, biproduct.ι_π]

Premises used: dif_pos, CategoryTheory.Limits.biproduct.ι_π
-- 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
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) 0
pos₁ :
  ∀ (h₁ : ¬j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 (eqToHom ⋯)
neg₁ :
  ∀ (h₁ : ¬j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 0
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)

Tactic:
split_ifs with h₁ h₂ 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
j : J
i : Subtype p
h : p j
h₁ : j = (↑i : J)
h₂ : Subtype.mk (p := p) j h = i
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)

Tactic:
rfl

Premises used: Subtype.restrict, 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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = (↑i : J)
h₂ : ¬Subtype.mk (p := p) j h = i
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) 0

Tactic:
False.elim (h₂ (Subtype.ext h₁))

Premises used: False.elim, Subtype.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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = (↑i : J)
h₂ : Subtype.mk (p := p) j h = i
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 (eqToHom ⋯)

Tactic:
False.elim (h₁ (congr_arg Subtype.val h₂))

Premises used: False.elim, congr_arg, Subtype.val
-- 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
j : J
i : Subtype p
h : p j
h₁ : ¬j = (↑i : J)
h₂ : ¬Subtype.mk (p := p) j h = i
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 0

Tactic:
rfl

Premises used: Subtype.restrict, 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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = (↑i : J)
h₂ : Subtype.mk (p := p) j h = i
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Premises used: 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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : ¬p j
neg :
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) 0
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
neg₁ :
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) 0
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
neg₂ neg₃ : Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 0
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))

Tactic:
rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]

Premises used: Eq.rec, dif_neg, CategoryTheory.Limits.zero_comp, Eq.symm, Subtype.property
-- 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
j : J
w :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
      (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) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
w₁ :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
pos :
  ∀ (i : Subtype p) (h : p j),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
neg neg₁ :
  ∀ (i : Subtype p) (h : ¬p j),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
    (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)

Tactic:
classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.toSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.zero_comp, 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)
inst_4 : DecidablePred p
⊢ ∀ (j : J),
    Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
        (desc fun (j : J) ↦
          if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))

Tactic:
simp
-- 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))
⊢ 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:
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 j_1 : Subtype p
w :
  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)
⊢ 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))

Tactic:
rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.toSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.lift_π
-- 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 j_1 : Subtype p
pos :
  ∀ (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 :
  ∀ (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₁ :
  ∀ (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₁ :
  ∀ (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) ⟶ 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)

Tactic:
split_ifs with h₁ h₂ 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)
j 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 ⋯)

Tactic:
rfl

Premises used: Subtype.restrict, 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 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

Tactic:
False.elim (h₂ (Subtype.ext h₁))

Premises used: False.elim, Subtype.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 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 ⋯)

Tactic:
False.elim (h₁ (congr_arg Subtype.val h₂))

Premises used: False.elim, congr_arg, Subtype.val
-- 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 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

Tactic:
rfl

Premises used: Subtype.restrict, 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 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 ⋯)

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Premises used: rfl