awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
have w : (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
Tactic: rcases Classical.em (i = j) with (rfl | h)
Cleared hypotheses: 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
w : (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
have w₁ : ∀ (h : ¬i = j), (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
Tactic: rcases Classical.em (i = j) with (rfl | h)
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
⊢ (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
have w : 0 ≫ ι f i ≫ s.π = ι f i ≫ s.π
Tactic: rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
w : 0 ≫ ι f i ≫ s.π = ι f i ≫ s.π
⊢ (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
have w₁ : 0 = ι f i ≫ s.π
Tactic: rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
w : 0 ≫ ι f i ≫ s.π = ι f i ≫ s.π
w₁ : 0 = ι f i ≫ s.π
⊢ (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π
have w₂ : Eq.{v + 1} (α := f i ⟶ s.pt) 0 0
Tactic: rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
h : ¬i = j
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
have w : 𝟙 (f j) ≫ ι f j ≫ s.π = ι f j ≫ s.π
Tactic: rw [if_pos (Ne.symm h), Category.id_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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
h : ¬i = j
w : 𝟙 (f j) ≫ ι f j ≫ s.π = ι f j ≫ s.π
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
have w₁ : ι f j ≫ s.π = ι f j ≫ s.π
Tactic: rw [if_pos (Ne.symm h), Category.id_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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
m :
  Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
      (CokernelCofork.ofπ (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ⟶
    s.pt
hm :
  Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯) ≫
      m =
    s.π
⊢ m = (fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π
have rw : m =
  𝟙 (biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)) ≫
    m
Tactic: rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]
-- 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, 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 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
⊢ 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, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg k.2]
        simp only [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
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, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg k.2]
        simp only [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
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, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg k.2]
        simp only [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
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'
have w₁ : ∀ (j : K),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        ((fun {x : C} (g : x ⟶ biproduct.{0, v, u} f)
              (x_1 :
                Eq (α := x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
                  (g ≫ biproduct.toSubtype f p) 0) ↦
            (g ≫ biproduct.toSubtype f pᶜ : x ⟶ biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f)))
          g' w)
        (biproduct.fromSubtype f pᶜ))
      (biproduct.π f j) =
    g' ≫ biproduct.π f j
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' : 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
have w₁ : (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
Tactic: simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]
-- 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' : 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
⊢ (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
have pos : ∀ (h : (p j)ᶜ), g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f j
Tactic: split_ifs with h
-- 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' : 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
pos : ∀ (h : (p j)ᶜ), g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f j
⊢ (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
have neg : ∀ (h : ¬(p j)ᶜ), g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j
Tactic: split_ifs with h