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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
w : ¬j = j'
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i))))
    0

Tactic:
simp [biproduct.ι_π_ne_assoc _ w]

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

Tactic:
rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π]

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

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

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

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

Premises used: CategoryTheory.Limits.comp_zero, Eq.rec, dif_neg, 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 w₁ w₂ :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f j)))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
w₃ :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
pos :
  ∀ (i : Subtype p) (h : p j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
neg neg₁ :
  ∀ (i : Subtype p) (h : ¬p j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f j))
    (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; dsimp
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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 (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]

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

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} (α := 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))
⊢ 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:
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} (α := 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)
⊢ 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))

Tactic:
rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]

Premises used: CategoryTheory.Limits.biproduct.fromSubtype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.ι_desc_assoc
-- 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_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 :
  ∀ (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₁ :
  ∀ (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₁ :
  ∀ (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} (α := 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)

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_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 ⋯)

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_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

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_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 ⋯)

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_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

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_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 ⋯)

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

Premises used: rfl