awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (hypothesis)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ biproduct.{0, v, u} f
w : Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p) 0
j : K
h : ¬(p j)ᶜ
⊢ g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j
have w₁ : Eq (α := W' ⟶ Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j sorry))
  (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
    (g' ≫ biproduct.toSubtype f p)
    (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j sorry)))
  (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) 0
    (biproduct.π (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j sorry)))
Tactic: replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
intro intro₁ intro₂ :
  ∀ {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),
    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'
⊢ ∀ {W' : C} (g' : W' ⟶ biproduct.{0, v, u} f)
    (eq' :
      Eq (α := W' ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f)) (g' ≫ biproduct.toSubtype f p)
        0),
    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' eq')
        (biproduct.fromSubtype f pᶜ) =
      g'
have w : ∀ {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),
  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: classical
        intro W' g' w
        ext j
        simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]
        split_ifs with h
        · simp
        · replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
          simpa using w.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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
have 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)))
Tactic: ext j k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
      (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)))
have 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
Tactic: simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
      (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
have 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
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
have w₁ : ¬(p (↑k : K))ᶜ
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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
have 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)))
Tactic: classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
have 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
Tactic: classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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
have 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
Tactic: classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
have w₃ : ∀ (j : Subtype pᶜ) (k : Subtype p), ¬(p (↑k : K))ᶜ
Tactic: classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
      (biproduct.toSubtype f pᶜ)
      ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
            (x_1 :
              Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                (biproduct.fromSubtype f p ≫ g) 0) ↦
          (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
        g' w) =
    g'
have w₁ : ∀ (j : K),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w)) =
    biproduct.ι f j ≫ g'
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w)) =
    biproduct.ι f j ≫ g'
have w₁ : (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
Tactic: simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]