awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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 ⋯)
⊢ 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)
have 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
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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))
have neg : Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom sorry 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)
Tactic: rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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)
⊢ 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))
have 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)
Tactic: rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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)
⊢ 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))
have neg₂ : Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) 0 0
Tactic: rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
    (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
⊢ 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)
have 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 sorry 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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
⊢ 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)
have 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 sorry 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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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))
⊢ 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)
have 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 sorry 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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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} (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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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))
have 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 sorry else 0) (if h : j_1 = j then eqToHom sorry else 0)
Tactic: rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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)
have 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 sorry) (eqToHom sorry)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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 ⋯)
⊢ 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)
have 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 sorry) 0
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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
⊢ 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)
have 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 sorry)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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 ⋯)
⊢ 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)
have 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
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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} (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)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
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)
have 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 sorry else 0) (if h : j_1 = j then eqToHom sorry else 0)
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]